Job 558

CakeML:6f5350e2f82b01a2630084750c447c8dd4aa1c5d
  Minor change to translation due to renaming in flat_elim [Nov 14 16:43:51]
#553 (flat-elim-cleanup)
Merging into:8ee5d433f5e6a93e9a41ea5e46b961c65130c2ef
  Merge pull request #551 from CakeML/translator-alist-tree [Nov 17 12:09:47]
HOL:e48aefc60b7c4a206ed939646485d31a341e2bfc
  Fully protect wordsLib's use of parser [Nov 17 11:30:47]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Nov 17 18:15:03 Claimed job
Nov 17 18:15:22 Building HOL
Nov 17 18:25:19 Starting developers/bin
Nov 17 18:26:35 Finished developers/bin                                        1m15s 916MB
Nov 17 18:26:36 Starting semantics/ffi
Nov 17 18:27:16 Finished semantics/ffi                                           39s 360MB
Nov 17 18:27:17 Starting semantics
Nov 17 18:28:54 Finished semantics                                             1m36s 926MB
Nov 17 18:28:55 Starting semantics/proofs
Nov 17 18:31:58 Finished semantics/proofs                                      3m02s   1GB
Nov 17 18:31:59 Starting basis/pure
Nov 17 18:35:51 Finished basis/pure                                            3m51s 603MB
Nov 17 18:35:52 Starting translator
Nov 17 18:39:11 Finished translator                                            3m18s   1GB
Nov 17 18:39:12 Starting compiler/parsing
Nov 17 18:40:44 Finished compiler/parsing                                      1m31s   1GB
Nov 17 18:40:45 Starting characteristic
Nov 17 18:43:28 Finished characteristic                                        2m42s   1GB
Nov 17 18:43:29 Starting translator/monadic
Nov 17 18:45:00 Finished translator/monadic                                    1m30s   1GB
Nov 17 18:45:01 Starting basis
Nov 17 19:02:14 Finished basis                                                17m12s   3GB
Nov 17 19:02:14 Starting compiler/inference
Nov 17 19:04:00 Finished compiler/inference                                    1m45s   1GB
Nov 17 19:04:01 Starting compiler/backend/reg_alloc
Nov 17 19:04:50 Finished compiler/backend/reg_alloc                              47s   1GB
Nov 17 19:04:50 Starting compiler/backend/gc
Nov 17 19:12:41 Finished compiler/backend/gc                                   7m49s   1GB
Nov 17 19:12:41 Starting compiler/backend
Nov 17 19:12:45 Finished compiler/backend                                         2s  26MB
Nov 17 19:12:45 Starting compiler/encoders/asm
Nov 17 19:12:47 Finished compiler/encoders/asm                                    1s  17MB
Nov 17 19:12:47 Starting compiler/encoders/x64
Nov 17 19:13:42 Finished compiler/encoders/x64                                   53s 584MB
Nov 17 19:13:43 Starting compiler/encoders/arm6
Nov 17 19:15:31 Finished compiler/encoders/arm6                                1m47s   1GB
Nov 17 19:15:32 Starting compiler/encoders/arm8
Nov 17 19:15:59 Finished compiler/encoders/arm8                                  26s 524MB
Nov 17 19:15:59 Starting compiler/encoders/mips
Nov 17 19:17:00 Finished compiler/encoders/mips                                  59s 874MB
Nov 17 19:17:00 Starting compiler/encoders/riscv
Nov 17 19:18:03 Finished compiler/encoders/riscv                               1m02s 712MB
Nov 17 19:18:04 Starting compiler/backend/x64
Nov 17 19:18:23 Finished compiler/backend/x64                                    18s   1GB
Nov 17 19:18:23 Starting compiler/backend/arm6
Nov 17 19:18:44 Finished compiler/backend/arm6                                   19s   1GB
Nov 17 19:18:44 Starting compiler/backend/arm8
Nov 17 19:19:05 Finished compiler/backend/arm8                                   19s   1GB
Nov 17 19:19:05 Starting compiler/backend/mips
Nov 17 19:19:25 Finished compiler/backend/mips                                   19s   1GB
Nov 17 19:19:26 Starting compiler/backend/riscv
Nov 17 19:19:46 Finished compiler/backend/riscv                                  19s   1GB
Nov 17 19:19:47 Starting compiler/parsing/proofs
Nov 17 19:25:55 Finished compiler/parsing/proofs                               6m07s   1GB
Nov 17 19:25:55 Starting compiler/inference/proofs
Nov 17 19:28:53 Finished compiler/inference/proofs                             2m57s 987MB
Nov 17 19:28:54 Starting compiler/backend/semantics
Nov 17 19:38:22 Finished compiler/backend/semantics                            9m27s   2GB
Nov 17 19:38:23 Starting compiler/backend/reg_alloc/proofs
Nov 17 19:41:10 Finished compiler/backend/reg_alloc/proofs                     2m47s 458MB
Nov 17 19:41:11 Starting compiler/backend/proofs
Nov 17 20:30:11 FAILED: compiler/backend/proofs
]0;Holmake: .]0;Holmake: ~/oven/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/machine-code/multiword]0;Holmake: ~/oven/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/machine-code/multiwordWorking in $(HOLDIR)/examples/machine-code/multiword
]0;Holmake: .]0;Holmake: ..]0;Holmake: ../../../basis/pure]0;Holmake: ~/oven/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/balanced_bst]0;Holmake: ~/oven/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/balanced_bstWorking in $(HOLDIR)/examples/balanced_bst
]0;Holmake: ~/oven/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/formal-languages]0;Holmake: ~/oven/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/formal-languagesWorking in $(HOLDIR)/examples/formal-languages
]0;Holmake: ~/oven/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/formal-languages/context-free]0;Holmake: ~/oven/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/formal-languages/context-freeWorking in $(HOLDIR)/examples/formal-languages/context-free
]0;Holmake: ~/oven/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/formal-languages/regularWorking in $(HOLDIR)/examples/formal-languages/regular
]0;Holmake: ../../../basis/pure]0;Holmake: ../../../misc]0;Holmake: ~/oven/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/oven/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: ../../../misc]0;Holmake: ../../../developers]0;Holmake: ../../../developersWorking in ../../../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]0;Holmake: ../../../characteristic]0;Holmake: ../../../compiler/parsing]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: ../../../compiler/parsing]0;Holmake: ../../../compiler/parsingWorking in $(CAKEMLDIR)/compiler/parsing
]0;Holmake: ../../../characteristic]0;Holmake: ../../../semantics/proofs]0;Holmake: ../../../semantics/proofsWorking in $(CAKEMLDIR)/semantics/proofs
]0;Holmake: ../../../characteristic]0;Holmake: ../../../translator]0;Holmake: ../../../semantics/alt_semantics/proofs]0;Holmake: ../../../semantics/alt_semantics]0;Holmake: ../../../semantics/alt_semanticsWorking in $(CAKEMLDIR)/semantics/alt_semantics
]0;Holmake: ../../../semantics/alt_semantics/proofs]0;Holmake: ../../../semantics/alt_semantics/proofsWorking in $(CAKEMLDIR)/semantics/alt_semantics/proofs
]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]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-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/l3-machine-code/common]0;Holmake: ~/oven/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/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: ..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: ../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
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 bvi_letProofTheory
bvi_letProofTheory                                                           OK
Starting work on clos_annotateProofTheory
data_liveProofTheory                                                         OK
Starting work on bvi_to_dataProofTheory
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
bvl_inlineProofTheory                                                        OK
Starting work on clos_knownPropsTheory
clos_knownPropsTheory                                                        OK
Starting work on clos_letopProofTheory
clos_fvsProofTheory                                                          OK
Starting work on clos_ticksProofTheory
clos_letopProofTheory                                                        OK
Starting work on clos_labelsProofTheory
clos_ticksProofTheory                                                        OK
Starting work on clos_knownProofTheory
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 bvl_jumpProofTheory
bvl_jumpProofTheory                                                          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
lab_filterProofTheory                                                        OK
Starting work on stack_removeProofTheory
data_to_word_memoryProofTheory                                               OK
Starting work on pat_to_closProofTheory
pat_to_closProofTheory                                                       OK
Starting work on source_to_flatProofTheory
flat_to_patProofTheory                                                       OK
Starting work on stack_allocProofTheory
source_to_flatProofTheory                                                    OK
Starting work on stack_namesProofTheory
stack_namesProofTheory                                                       OK
Starting work on word_to_stackProofTheory
stack_removeProofTheory                                                      OK
Starting work on lab_to_targetProofTheory
word_allocProofTheory                                                        OK
Starting work on word_to_wordProofTheory
word_to_wordProofTheory                                                      OK
Starting work on data_to_word_gcProofTheory
lab_to_targetProofTheory                                                     OK
Starting work on word_elimProofTheory
stack_allocProofTheory                                                       OK
data_to_word_gcProofTheory                                                   OK
Starting work on data_to_word_bignumProofTheory
Starting work on stack_to_labProofTheory
word_elimProofTheory                                                         OK
data_to_word_bignumProofTheory                                               OK
Starting work on data_to_word_assignProofTheory
stack_to_labProofTheory                                                      OK
word_to_stackProofTheory                                                     OK
data_to_word_assignProofTheory                                               OK
Starting work on data_to_wordProofTheory
data_to_wordProofTheory                                                      OK
Starting work on backendProofTheory
backendProofTheory                                                  FAILED! <1>
      "compile_correct",
      [
         QUOTE
         " (*#loc 3746 4*)compile (c:'a config) prog = SOME (bytes,bitmaps,c') \226\135\146\n   let (s,env) = THE (prim_sem_env (ffi:'ffi ffi_state)) in\n   \194\172semantics_prog s env prog Fail \226\136\167\n   backend_config_ok c \226\136\167 mc_conf_ok mc \226\136\167 mc_init_ok c mc \226\136\167\n   installed bytes cbspace bitmaps data_sp c'.ffi_names ffi (heap_regs c.stack_conf.reg_names) mc ms \226\135\146\n     machine_sem (mc:(\206\177,\206\178,\206\179) machine_config) ffi ms \226\138\134\n       extend_with_resource_limit (semantics_prog s env prog)"
         ],
      ... \\ ... \\ ... ...
      )
 error in quse /home/cake/oven/regression/cakeml-558/compiler/backend/proofs/backendProofScript.sml : Fail "Static Errors"
 error in load backendProofScript : Fail "Static Errors"
 Uncaught exception: Fail "Static Errors"