CakeML Regression Test

Job 945

CakeML:30116436c1419304b8c1396c4f8f19cd3a43dbf7
  Remove last cheat [Jul 21 20:27:27]
#670 (refactor-flat)
Merging into:7fd70910f8d379bf4ebecddca50b24450bf1bb16
  Merge pull request #668 from CakeML/trans-char-list [Jul 18 13:59:56]
HOL:b9f1c2fc0eba7f6f95c4f1890012f7a1f1dbf3cc
  guessing encapsulating structure namespace [Jul 21 15:19:14]
Machine:te1

Jul 21 20:30:07 Claimed job
Jul 21 20:30:15 Building HOL
Jul 21 20:43:31 Starting developers
Jul 21 20:43:34 Finished developers                                               2s  32MB
Jul 21 20:43:34 Starting developers/bin
Jul 21 20:43:41 Finished developers/bin                                           7s 965MB
Jul 21 20:43:41 Starting semantics/ffi
Jul 21 20:44:36 Finished semantics/ffi                                           55s 589MB
Jul 21 20:44:36 Starting semantics
Jul 21 20:46:50 Finished semantics                                             2m13s   1GB
Jul 21 20:46:50 Starting semantics/proofs
Jul 21 20:51:24 Finished semantics/proofs                                      4m33s   1GB
Jul 21 20:51:24 Starting semantics/alt_semantics
Jul 21 20:51:35 Finished semantics/alt_semantics                                 10s 315MB
Jul 21 20:51:35 Starting semantics/alt_semantics/proofs
Jul 21 20:54:09 Finished semantics/alt_semantics/proofs                        2m33s 835MB
Jul 21 20:54:09 Starting basis/pure
Jul 21 20:59:12 Finished basis/pure                                            5m02s 744MB
Jul 21 20:59:12 Starting translator
Jul 21 21:01:40 Finished translator                                            2m28s   1GB
Jul 21 21:01:40 Starting compiler/parsing
Jul 21 21:02:58 Finished compiler/parsing                                      1m17s   1GB
Jul 21 21:02:58 Starting characteristic
Jul 21 21:10:22 Finished characteristic                                        7m23s   2GB
Jul 21 21:10:22 Starting translator/monadic
Jul 21 21:12:28 Finished translator/monadic                                    2m06s   1GB
Jul 21 21:12:28 Starting basis
Jul 21 21:35:56 Finished basis                                                23m27s   2GB
Jul 21 21:35:56 Starting compiler/inference
Jul 21 21:38:39 Finished compiler/inference                                    2m42s   1GB
Jul 21 21:38:39 Starting compiler/backend/reg_alloc
Jul 21 21:40:01 Finished compiler/backend/reg_alloc                            1m21s   1GB
Jul 21 21:40:01 Starting compiler/backend/gc
Jul 21 21:53:13 Finished compiler/backend/gc                                  13m12s   1GB
Jul 21 21:53:13 Starting compiler/backend
Jul 21 21:53:16 Finished compiler/backend                                         2s  33MB
Jul 21 21:53:16 Starting compiler/encoders/asm
Jul 21 21:53:17 Finished compiler/encoders/asm                                    1s  24MB
Jul 21 21:53:17 Starting compiler/encoders/x64
Jul 21 21:54:45 Finished compiler/encoders/x64                                 1m28s 988MB
Jul 21 21:54:45 Starting compiler/encoders/arm7
Jul 21 21:57:12 Finished compiler/encoders/arm7                                2m26s   1GB
Jul 21 21:57:12 Starting compiler/encoders/arm8
Jul 21 21:57:59 Finished compiler/encoders/arm8                                  46s 552MB
Jul 21 21:57:59 Starting compiler/encoders/mips
Jul 21 21:59:39 Finished compiler/encoders/mips                                1m39s   1GB
Jul 21 21:59:39 Starting compiler/encoders/riscv
Jul 21 22:01:34 Finished compiler/encoders/riscv                               1m54s   1GB
Jul 21 22:01:34 Starting compiler/encoders/ag32
Jul 21 22:01:58 Finished compiler/encoders/ag32                                  24s 770MB
Jul 21 22:01:58 Starting compiler/backend/x64
Jul 21 22:02:24 Finished compiler/backend/x64                                    25s   1GB
Jul 21 22:02:24 Starting compiler/backend/arm7
Jul 21 22:02:52 Finished compiler/backend/arm7                                   27s   1GB
Jul 21 22:02:52 Starting compiler/backend/arm8
Jul 21 22:03:18 Finished compiler/backend/arm8                                   25s   1GB
Jul 21 22:03:18 Starting compiler/backend/mips
Jul 21 22:03:45 Finished compiler/backend/mips                                   27s   1GB
Jul 21 22:03:45 Starting compiler/backend/riscv
Jul 21 22:04:11 Finished compiler/backend/riscv                                  25s   1GB
Jul 21 22:04:11 Starting compiler/backend/ag32
Jul 21 22:05:42 Finished compiler/backend/ag32                                 1m31s   1GB
Jul 21 22:05:43 Starting compiler/parsing/proofs
Jul 21 22:14:30 Finished compiler/parsing/proofs                               8m46s 995MB
Jul 21 22:14:30 Starting compiler/inference/proofs
Jul 21 22:18:31 Finished compiler/inference/proofs                             4m00s   1GB
Jul 21 22:18:31 Starting compiler/backend/semantics
Jul 21 22:28:10 Finished compiler/backend/semantics                            9m39s   1GB
Jul 21 22:28:10 Starting compiler/backend/reg_alloc/proofs
Jul 21 22:32:57 Finished compiler/backend/reg_alloc/proofs                     4m46s   1GB
Jul 21 22:32:57 Starting compiler/backend/proofs
Jul 21 23:23:14 FAILED: compiler/backend/proofs
]0;Holmake: .]0;Holmake: ~/regression-worker/HOL-b9f1c2fc0eba7f6f95c4f1890012f7a1f1dbf3cc/examples/machine-code/multiword]0;Holmake: ~/regression-worker/HOL-b9f1c2fc0eba7f6f95c4f1890012f7a1f1dbf3cc/examples/machine-code/multiword[1mWorking in $(HOLDIR)/examples/machine-code/multiword[0m
]0;Holmake: .]0;Holmake: ..]0;Holmake: ~/regression-worker/cakeml-945/basis/pure]0;Holmake: ~/regression-worker/HOL-b9f1c2fc0eba7f6f95c4f1890012f7a1f1dbf3cc/examples/balanced_bst]0;Holmake: ~/regression-worker/HOL-b9f1c2fc0eba7f6f95c4f1890012f7a1f1dbf3cc/examples/balanced_bst[1mWorking in $(HOLDIR)/examples/balanced_bst[0m
]0;Holmake: ~/regression-worker/cakeml-945/basis/pure]0;Holmake: ~/regression-worker/HOL-b9f1c2fc0eba7f6f95c4f1890012f7a1f1dbf3cc/examples/formal-languages/regular]0;Holmake: ~/regression-worker/HOL-b9f1c2fc0eba7f6f95c4f1890012f7a1f1dbf3cc/examples/formal-languages]0;Holmake: ~/regression-worker/HOL-b9f1c2fc0eba7f6f95c4f1890012f7a1f1dbf3cc/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression-worker/HOL-b9f1c2fc0eba7f6f95c4f1890012f7a1f1dbf3cc/examples/formal-languages/regular]0;Holmake: ~/regression-worker/HOL-b9f1c2fc0eba7f6f95c4f1890012f7a1f1dbf3cc/examples/formal-languages/context-free]0;Holmake: ~/regression-worker/HOL-b9f1c2fc0eba7f6f95c4f1890012f7a1f1dbf3cc/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression-worker/HOL-b9f1c2fc0eba7f6f95c4f1890012f7a1f1dbf3cc/examples/formal-languages/regular]0;Holmake: ~/regression-worker/HOL-b9f1c2fc0eba7f6f95c4f1890012f7a1f1dbf3cc/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ~/regression-worker/cakeml-945/basis/pure]0;Holmake: ~/regression-worker/cakeml-945/misc]0;Holmake: ~/regression-worker/HOL-b9f1c2fc0eba7f6f95c4f1890012f7a1f1dbf3cc/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression-worker/HOL-b9f1c2fc0eba7f6f95c4f1890012f7a1f1dbf3cc/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/regression-worker/cakeml-945/misc]0;Holmake: ~/regression-worker/cakeml-945/developers]0;Holmake: ~/regression-worker/cakeml-945/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression-worker/cakeml-945/misc]0;Holmake: ~/regression-worker/cakeml-945/misc/lem_lib_stub]0;Holmake: ~/regression-worker/cakeml-945/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression-worker/cakeml-945/misc]0;Holmake: ~/regression-worker/cakeml-945/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ~/regression-worker/cakeml-945/basis/pure]0;Holmake: ~/regression-worker/cakeml-945/basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ..]0;Holmake: ../reg_alloc]0;Holmake: ~/regression-worker/cakeml-945/translator/monadic/monad_base]0;Holmake: ~/regression-worker/cakeml-945/semantics]0;Holmake: ~/regression-worker/cakeml-945/semantics/ffi]0;Holmake: ~/regression-worker/cakeml-945/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression-worker/cakeml-945/semantics]0;Holmake: ~/regression-worker/cakeml-945/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ~/regression-worker/cakeml-945/translator/monadic/monad_base]0;Holmake: ~/regression-worker/cakeml-945/translator/monadic/monad_base[1mWorking in $(CAKEMLDIR)/translator/monadic/monad_base[0m
]0;Holmake: ../reg_alloc]0;Holmake: ~/regression-worker/cakeml-945/unverified/reg_alloc]0;Holmake: ~/regression-worker/cakeml-945/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-worker/HOL-b9f1c2fc0eba7f6f95c4f1890012f7a1f1dbf3cc/examples/l3-machine-code/common]0;Holmake: ~/regression-worker/HOL-b9f1c2fc0eba7f6f95c4f1890012f7a1f1dbf3cc/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-worker/cakeml-945/semantics/proofs]0;Holmake: ~/regression-worker/cakeml-945/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-worker/cakeml-945/translator/monadic]0;Holmake: ~/regression-worker/cakeml-945/characteristic]0;Holmake: ~/regression-worker/cakeml-945/compiler/parsing]0;Holmake: ~/regression-worker/cakeml-945/compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ~/regression-worker/cakeml-945/characteristic]0;Holmake: ~/regression-worker/cakeml-945/translator]0;Holmake: ~/regression-worker/cakeml-945/translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ~/regression-worker/cakeml-945/characteristic]0;Holmake: ~/regression-worker/cakeml-945/characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: ~/regression-worker/cakeml-945/translator/monadic]0;Holmake: ~/regression-worker/cakeml-945/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
stack_namesProofTheory                                                                                                                                                                       OK
Starting work on word_to_stackProofTheory
word_allocProofTheory                                                                                                                                                                        OK
Starting work on word_to_wordProofTheory
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 word_elimProofTheory
stack_allocProofTheory                                                                                                                                                                       OK
Starting work on README.md
README.md                                                                                                                                                                                    OK
word_elimProofTheory                                                                                                                                                                         OK
data_to_word_bignumProofTheory                                                                                                                                                               OK
Starting work on data_to_word_assignProofTheory
word_to_stackProofTheory                                                                                                                                                                     OK
Starting work on stack_to_labProofTheory
stack_to_labProofTheory                                                                                                                                                                      OK
data_to_word_assignProofTheory                                                                                                                                                               OK
Starting work on data_to_wordProofTheory
data_to_wordProofTheory                                                                                                                                                                      OK
Starting work on backendProofTheory
backendProofTheory                                                                                                                                                                  FAILED! <1>
    semantics_prog s env prog Fail  backend_config_ok c 
    lab_to_targetProof$mc_conf_ok mc  mc_init_ok c mc 
    installed bytes cbspace bitmaps data_sp c'.ffi_names ffi
      (heap_regs c.stack_conf.reg_names) mc ms 
    machine_sem mc ffi ms 
    extend_with_resource_limit (semantics_prog s env prog))
 
 failed.
 Failed to prove theorem compile_correct.
 Uncaught exception: HOL_ERR {message = "by's tactic failed to prove subgoal on line 359 (THEN1 on line 500) (THEN1 on line 517) (THEN1 on line 693) (THEN1 on line 807) (THEN1 on line 818) (THEN1 on line 825) (THEN1 on line 927) (THEN1 on line 1021) (THEN1 on line 1072) (THEN1 on line 1596) (THEN1 on line 1806) (THEN1 on line 1819) (THEN1 on line 1844) (THEN1 on line 1960)", origin_function = "by", origin_structure = "BasicProvers"}