Job 619

CakeML:726e2d5b2688f471f56c465bbd919a1113255f51
  Merge branch 'origin/master' into local [Dec 08 22:32:12]
#577 (local)
Merging into:49d90bdd0995c89747b24d60ef7a2765e3afc6ca
  Merge pull request #578 from CakeML/cleanup [Dec 08 09:01:35]
HOL:392753738a23ad83e605a7549b19c415f90faf6b
  Fix Vim mode for Theorem quote filter hack [Dec 05 19:40:50]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Dec 09 01:15:02 Claimed job
Dec 09 01:15:22 Reusing HOL
Dec 09 01:16:13 Starting developers
Dec 09 01:16:16 Finished developers                                               2s  21MB
Dec 09 01:16:16 Starting developers/bin
Dec 09 01:17:31 Finished developers/bin                                        1m14s 916MB
Dec 09 01:17:32 Starting semantics/ffi
Dec 09 01:17:43 Finished semantics/ffi                                           10s 206MB
Dec 09 01:17:43 Starting semantics
Dec 09 01:19:03 Finished semantics                                             1m18s 810MB
Dec 09 01:19:04 Starting semantics/proofs
Dec 09 01:22:05 Finished semantics/proofs                                      3m00s   1GB
Dec 09 01:22:06 Starting basis/pure
Dec 09 01:22:59 Finished basis/pure                                              52s 715MB
Dec 09 01:22:59 Starting translator
Dec 09 01:24:15 Finished translator                                            1m14s 914MB
Dec 09 01:24:15 Starting compiler/parsing
Dec 09 01:25:33 Finished compiler/parsing                                      1m16s   1GB
Dec 09 01:25:33 Starting characteristic
Dec 09 01:28:07 Finished characteristic                                        2m32s   1GB
Dec 09 01:28:07 Starting translator/monadic
Dec 09 01:29:36 Finished translator/monadic                                    1m27s   1GB
Dec 09 01:29:36 Starting basis
Dec 09 01:45:44 Finished basis                                                16m06s   3GB
Dec 09 01:45:44 Starting compiler/inference
Dec 09 01:47:27 Finished compiler/inference                                    1m42s   1GB
Dec 09 01:47:28 Starting compiler/backend/reg_alloc
Dec 09 01:48:15 Finished compiler/backend/reg_alloc                              46s 948MB
Dec 09 01:48:16 Starting compiler/backend/gc
Dec 09 01:54:40 Finished compiler/backend/gc                                   6m23s   1GB
Dec 09 01:54:41 Starting compiler/backend
Dec 09 01:54:44 Finished compiler/backend                                         2s  16MB
Dec 09 01:54:44 Starting compiler/encoders/asm
Dec 09 01:54:46 Finished compiler/encoders/asm                                    1s  12MB
Dec 09 01:54:47 Starting compiler/encoders/x64
Dec 09 01:55:03 Finished compiler/encoders/x64                                   15s 372MB
Dec 09 01:55:04 Starting compiler/encoders/arm6
Dec 09 01:55:47 Finished compiler/encoders/arm6                                  42s 431MB
Dec 09 01:55:48 Starting compiler/encoders/arm8
Dec 09 01:55:57 Finished compiler/encoders/arm8                                   8s 337MB
Dec 09 01:55:57 Starting compiler/encoders/mips
Dec 09 01:56:08 Finished compiler/encoders/mips                                   9s 525MB
Dec 09 01:56:08 Starting compiler/encoders/riscv
Dec 09 01:56:18 Finished compiler/encoders/riscv                                  8s 412MB
Dec 09 01:56:18 Starting compiler/encoders/ag32
Dec 09 01:56:36 Finished compiler/encoders/ag32                                  16s 510MB
Dec 09 01:56:37 Starting compiler/backend/x64
Dec 09 01:56:55 Finished compiler/backend/x64                                    18s 839MB
Dec 09 01:56:56 Starting compiler/backend/arm6
Dec 09 01:57:15 Finished compiler/backend/arm6                                   18s   1GB
Dec 09 01:57:16 Starting compiler/backend/arm8
Dec 09 01:57:35 Finished compiler/backend/arm8                                   18s   1GB
Dec 09 01:57:36 Starting compiler/backend/mips
Dec 09 01:57:56 Finished compiler/backend/mips                                   19s   1GB
Dec 09 01:57:56 Starting compiler/backend/riscv
Dec 09 01:58:15 Finished compiler/backend/riscv                                  18s   1GB
Dec 09 01:58:16 Starting compiler/backend/ag32
Dec 09 01:59:26 Finished compiler/backend/ag32                                 1m09s   1GB
Dec 09 01:59:27 Starting compiler/parsing/proofs
Dec 09 02:05:38 Finished compiler/parsing/proofs                               6m09s 793MB
Dec 09 02:05:38 Starting compiler/inference/proofs
Dec 09 02:08:28 Finished compiler/inference/proofs                             2m49s   1GB
Dec 09 02:08:29 Starting compiler/backend/semantics
Dec 09 02:17:21 Finished compiler/backend/semantics                            8m51s   2GB
Dec 09 02:17:21 Starting compiler/backend/reg_alloc/proofs
Dec 09 02:20:06 Finished compiler/backend/reg_alloc/proofs                     2m43s 661MB
Dec 09 02:20:06 Starting compiler/backend/proofs
Dec 09 10:11:03 FAILED: compiler/backend/proofs
]0;Holmake: .]0;Holmake: ~/oven/regression/HOL-392753738a23ad83e605a7549b19c415f90faf6b/examples/machine-code/multiword]0;Holmake: ~/oven/regression/HOL-392753738a23ad83e605a7549b19c415f90faf6b/examples/machine-code/multiwordWorking in $(HOLDIR)/examples/machine-code/multiword
]0;Holmake: .]0;Holmake: ..]0;Holmake: ../../../basis/pure]0;Holmake: ~/oven/regression/HOL-392753738a23ad83e605a7549b19c415f90faf6b/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-392753738a23ad83e605a7549b19c415f90faf6b/examples/balanced_bst]0;Holmake: ~/oven/regression/HOL-392753738a23ad83e605a7549b19c415f90faf6b/examples/balanced_bstWorking in $(HOLDIR)/examples/balanced_bst
]0;Holmake: ~/oven/regression/HOL-392753738a23ad83e605a7549b19c415f90faf6b/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-392753738a23ad83e605a7549b19c415f90faf6b/examples/formal-languages]0;Holmake: ~/oven/regression/HOL-392753738a23ad83e605a7549b19c415f90faf6b/examples/formal-languagesWorking in $(HOLDIR)/examples/formal-languages
]0;Holmake: ~/oven/regression/HOL-392753738a23ad83e605a7549b19c415f90faf6b/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-392753738a23ad83e605a7549b19c415f90faf6b/examples/formal-languages/context-free]0;Holmake: ~/oven/regression/HOL-392753738a23ad83e605a7549b19c415f90faf6b/examples/formal-languages/context-freeWorking in $(HOLDIR)/examples/formal-languages/context-free
]0;Holmake: ~/oven/regression/HOL-392753738a23ad83e605a7549b19c415f90faf6b/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-392753738a23ad83e605a7549b19c415f90faf6b/examples/formal-languages/regularWorking in $(HOLDIR)/examples/formal-languages/regular
]0;Holmake: ../../../basis/pure]0;Holmake: ../../../misc]0;Holmake: ~/oven/regression/HOL-392753738a23ad83e605a7549b19c415f90faf6b/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/oven/regression/HOL-392753738a23ad83e605a7549b19c415f90faf6b/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: ../../../misc]0;Holmake: ../../../developers]0;Holmake: ../../../developersWorking in $(CAKEMLDIR)/developers
]0;Holmake: ../../../misc]0;Holmake: ../../../misc/lem_lib_stub]0;Holmake: ../../../misc/lem_lib_stubWorking in $(CAKEMLDIR)/misc/lem_lib_stub
]0;Holmake: ../../../misc]0;Holmake: ../../../miscWorking in $(CAKEMLDIR)/misc
]0;Holmake: ../../../basis/pure]0;Holmake: ../../../basis/pureWorking in $(CAKEMLDIR)/basis/pure
]0;Holmake: ..]0;Holmake: ../reg_alloc]0;Holmake: ../../../translator/monadic/monad_base]0;Holmake: ../../../semantics]0;Holmake: ../../../semantics/ffi]0;Holmake: ../../../semantics/ffiWorking in $(CAKEMLDIR)/semantics/ffi
]0;Holmake: ../../../semantics]0;Holmake: ../../../semanticsWorking in $(CAKEMLDIR)/semantics
]0;Holmake: ../../../translator/monadic/monad_base]0;Holmake: ../../../translator/monadic/monad_baseWorking in $(CAKEMLDIR)/translator/monadic/monad_base
]0;Holmake: ../reg_alloc]0;Holmake: ../../../unverified/reg_alloc]0;Holmake: ../../../unverified/reg_allocWorking in $(CAKEMLDIR)/unverified/reg_alloc
]0;Holmake: ../reg_alloc]0;Holmake: ../reg_allocWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc
]0;Holmake: ..]0;Holmake: ../../encoders/asm]0;Holmake: ~/oven/regression/HOL-392753738a23ad83e605a7549b19c415f90faf6b/examples/l3-machine-code/common]0;Holmake: ~/oven/regression/HOL-392753738a23ad83e605a7549b19c415f90faf6b/examples/l3-machine-code/commonWorking in $(HOLDIR)/examples/l3-machine-code/common
]0;Holmake: ../../encoders/asm]0;Holmake: ../../encoders/asmWorking in $(CAKEMLDIR)/compiler/encoders/asm
]0;Holmake: ..]0;Holmake: ../../../semantics/proofs]0;Holmake: ../../../semantics/proofsWorking in $(CAKEMLDIR)/semantics/proofs
]0;Holmake: ..]0;Holmake: ..Working in $(CAKEMLDIR)/compiler/backend
]0;Holmake: .]0;Holmake: ../gc]0;Holmake: ../gcWorking in $(CAKEMLDIR)/compiler/backend/gc
]0;Holmake: .]0;Holmake: ../reg_alloc/proofs]0;Holmake: ../../../translator/monadic]0;Holmake: ../../../characteristic]0;Holmake: ../../../compiler/parsing]0;Holmake: ../../../compiler/parsingWorking in $(CAKEMLDIR)/compiler/parsing
]0;Holmake: ../../../characteristic]0;Holmake: ../../../translator]0;Holmake: ../../../translatorWorking in $(CAKEMLDIR)/translator
]0;Holmake: ../../../characteristic]0;Holmake: ../../../characteristicWorking in $(CAKEMLDIR)/characteristic
]0;Holmake: ../../../translator/monadic]0;Holmake: ../../../translator/monadicWorking in $(CAKEMLDIR)/translator/monadic
]0;Holmake: ../reg_alloc/proofs]0;Holmake: ../reg_alloc/proofsWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
]0;Holmake: .]0;Holmake: ../semantics]0;Holmake: ../semanticsWorking in $(CAKEMLDIR)/compiler/backend/semantics
]0;Holmake: .]0;Holmake: .Working in $(CAKEMLDIR)/compiler/backend/proofs
Starting work on heap
Starting work on README.md
README.md                                                                    OK
heap                                                                         OK
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
clos_annotateProofTheory                                                     OK
Starting work on clos_callProofTheory
bvl_constProofTheory                                                         OK
Starting work on bvl_handleProofTheory
bvl_handleProofTheory                                                        OK
Starting work on bvl_inlineProofTheory
bvi_to_dataProofTheory                                                       OK
Starting work on clos_fvsProofTheory
clos_fvsProofTheory                                                          OK
Starting work on clos_knownPropsTheory
bvl_inlineProofTheory                                                        OK
Starting work on clos_letopProofTheory
clos_letopProofTheory                                                        OK
Starting work on clos_ticksProofTheory
clos_ticksProofTheory                                                        OK
Starting work on clos_labelsProofTheory
clos_labelsProofTheory                                                       OK
Starting work on clos_mtiProofTheory
clos_mtiProofTheory                                                          OK
Starting work on clos_numberProofTheory
bvi_tailrecProofTheory                                                       OK
Starting work on bvl_to_bviProofTheory
clos_numberProofTheory                                                       OK
Starting work on word_simpProofTheory
word_simpProofTheory                                                         OK
Starting work on word_gcFunctionsTheory
clos_callProofTheory                                                         OK
Starting work on word_bignumProofTheory
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
word_instProofTheory                                                         OK
Starting work on word_removeProofTheory
word_removeProofTheory                                                       OK
Starting work on flat_elimProofTheory
flat_elimProofTheory                                                         OK
Starting work on flat_exh_matchProofTheory
data_to_word_memoryProofTheory                                               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
lab_filterProofTheory                                                        OK
Starting work on stack_removeProofTheory
flat_to_patProofTheory                                                       OK
Starting work on pat_to_closProofTheory
pat_to_closProofTheory                                                       OK
Starting work on source_to_flatProofTheory
word_allocProofTheory                                                        OK
Starting work on word_to_wordProofTheory
source_to_flatProofTheory                                                    OK
Starting work on stack_allocProofTheory
word_to_wordProofTheory                                                      OK
Starting work on data_to_word_gcProofTheory
stack_removeProofTheory                                                      OK
Starting work on lab_to_targetProofTheory
data_to_word_gcProofTheory                                                   OK
Starting work on data_to_word_bignumProofTheory
lab_to_targetProofTheory                                                     OK
Starting work on stack_namesProofTheory
data_to_word_bignumProofTheory                                               OK
Starting work on data_to_word_assignProofTheory
stack_allocProofTheory                                                       OK
Starting work on word_to_stackProofTheory
stack_namesProofTheory                                                       OK
Starting work on word_elimProofTheory
word_elimProofTheory                                                         OK
word_to_stackProofTheory                                                     OK
Starting work on stack_to_labProofTheory
data_to_word_assignProofTheory                                               OK
Starting work on data_to_wordProofTheory
data_to_wordProofTheory                                                      OK
stack_to_labProofTheory                                                      OK