Job 874

CakeML:45b1619f37337d72ec309252e0e4c5351906545c
  Fit patLang semantics for FMA [May 15 07:58:54]
#633 (FMA_support)
Merging into:8f8560b3414274dcffa62719ba224df92d8cb039
  Merge pull request #651 from talsewell/translator_messages [May 15 03:55:41]
HOL:1557f72fc9a7a80bc5ce2e4df30afd51803c8b75
  Get formal-languages/regular to pass src tests again [May 09 11:06:43]
Machine:te1

May 15 19:19:11 Claimed job
May 15 19:19:15 Reusing HOL
May 15 19:20:03 Starting developers
May 15 19:20:06 Finished developers                                               2s  32MB
May 15 19:20:06 Starting developers/bin
May 15 19:20:12 Finished developers/bin                                           6s 926MB
May 15 19:20:12 Starting semantics/ffi
May 15 19:20:26 Finished semantics/ffi                                           13s 266MB
May 15 19:20:26 Starting semantics
May 15 19:22:20 Finished semantics                                             1m53s   1GB
May 15 19:22:20 Starting semantics/proofs
May 15 19:26:41 Finished semantics/proofs                                      4m20s   1GB
May 15 19:26:41 Starting basis/pure
May 15 19:27:47 Finished basis/pure                                            1m05s 773MB
May 15 19:27:47 Starting translator
May 15 19:30:06 Finished translator                                            2m18s   1GB
May 15 19:30:06 Starting compiler/parsing
May 15 19:31:24 Finished compiler/parsing                                      1m17s   2GB
May 15 19:31:24 Starting characteristic
May 15 19:38:46 Finished characteristic                                        7m22s   1GB
May 15 19:38:46 Starting translator/monadic
May 15 19:40:56 Finished translator/monadic                                    2m09s   1GB
May 15 19:40:56 Starting basis
May 15 20:04:15 Finished basis                                                23m18s   2GB
May 15 20:04:15 Starting compiler/inference
May 15 20:06:24 Finished compiler/inference                                    2m09s   1GB
May 15 20:06:24 Starting compiler/backend/reg_alloc
May 15 20:07:42 Finished compiler/backend/reg_alloc                            1m17s   1GB
May 15 20:07:42 Starting compiler/backend/gc
May 15 20:18:39 Finished compiler/backend/gc                                  10m57s   2GB
May 15 20:18:39 Starting compiler/backend
May 15 20:18:42 Finished compiler/backend                                         2s  35MB
May 15 20:18:42 Starting compiler/encoders/asm
May 15 20:18:43 Finished compiler/encoders/asm                                    1s  32MB
May 15 20:18:43 Starting compiler/encoders/x64
May 15 20:19:18 Finished compiler/encoders/x64                                   34s 748MB
May 15 20:19:18 Starting compiler/encoders/arm7
May 15 20:20:22 Finished compiler/encoders/arm7                                1m04s   1GB
May 15 20:20:23 Starting compiler/encoders/arm8
May 15 20:20:41 Finished compiler/encoders/arm8                                  17s 602MB
May 15 20:20:41 Starting compiler/encoders/mips
May 15 20:21:05 Finished compiler/encoders/mips                                  24s   1GB
May 15 20:21:06 Starting compiler/encoders/riscv
May 15 20:21:25 Finished compiler/encoders/riscv                                 19s 811MB
May 15 20:21:25 Starting compiler/encoders/ag32
May 15 20:21:49 Finished compiler/encoders/ag32                                  23s 498MB
May 15 20:21:49 Starting compiler/backend/x64
May 15 20:22:14 Finished compiler/backend/x64                                    24s   1GB
May 15 20:22:14 Starting compiler/backend/arm7
May 15 20:22:40 Finished compiler/backend/arm7                                   26s   1GB
May 15 20:22:40 Starting compiler/backend/arm8
May 15 20:23:07 Finished compiler/backend/arm8                                   26s   1GB
May 15 20:23:07 Starting compiler/backend/mips
May 15 20:23:32 Finished compiler/backend/mips                                   25s 948MB
May 15 20:23:32 Starting compiler/backend/riscv
May 15 20:23:59 Finished compiler/backend/riscv                                  26s   1GB
May 15 20:23:59 Starting compiler/backend/ag32
May 15 20:25:30 Finished compiler/backend/ag32                                 1m31s   1GB
May 15 20:25:30 Starting compiler/parsing/proofs
May 15 20:34:11 Finished compiler/parsing/proofs                               8m40s   1GB
May 15 20:34:11 Starting compiler/inference/proofs
May 15 20:38:08 Finished compiler/inference/proofs                             3m56s   1GB
May 15 20:38:08 Starting compiler/backend/semantics
May 15 20:47:29 Finished compiler/backend/semantics                            9m20s   1GB
May 15 20:47:29 Starting compiler/backend/reg_alloc/proofs
May 15 20:52:11 Finished compiler/backend/reg_alloc/proofs                     4m42s 920MB
May 15 20:52:11 Starting compiler/backend/proofs
May 15 21:30:28 FAILED: compiler/backend/proofs
]0;Holmake: .]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/machine-code/multiword]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/machine-code/multiword[1mWorking in $(HOLDIR)/examples/machine-code/multiword[0m
]0;Holmake: .]0;Holmake: ..]0;Holmake: ~/regression-worker/cakeml-874/basis/pure]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/balanced_bst]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/balanced_bst[1mWorking in $(HOLDIR)/examples/balanced_bst[0m
]0;Holmake: ~/regression-worker/cakeml-874/basis/pure]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/formal-languages/regular]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/formal-languages]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/formal-languages/regular]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/formal-languages/context-free]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/formal-languages/regular]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ~/regression-worker/cakeml-874/basis/pure]0;Holmake: ~/regression-worker/cakeml-874/misc]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/regression-worker/cakeml-874/misc]0;Holmake: ~/regression-worker/cakeml-874/developers]0;Holmake: ~/regression-worker/cakeml-874/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression-worker/cakeml-874/misc]0;Holmake: ~/regression-worker/cakeml-874/misc/lem_lib_stub]0;Holmake: ~/regression-worker/cakeml-874/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression-worker/cakeml-874/misc]0;Holmake: ~/regression-worker/cakeml-874/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ~/regression-worker/cakeml-874/basis/pure]0;Holmake: ~/regression-worker/cakeml-874/basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ..]0;Holmake: ../reg_alloc]0;Holmake: ~/regression-worker/cakeml-874/translator/monadic/monad_base]0;Holmake: ~/regression-worker/cakeml-874/semantics]0;Holmake: ~/regression-worker/cakeml-874/semantics/ffi]0;Holmake: ~/regression-worker/cakeml-874/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression-worker/cakeml-874/semantics]0;Holmake: ~/regression-worker/cakeml-874/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ~/regression-worker/cakeml-874/translator/monadic/monad_base]0;Holmake: ~/regression-worker/cakeml-874/translator/monadic/monad_base[1mWorking in $(CAKEMLDIR)/translator/monadic/monad_base[0m
]0;Holmake: ../reg_alloc]0;Holmake: ~/regression-worker/cakeml-874/unverified/reg_alloc]0;Holmake: ~/regression-worker/cakeml-874/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-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/common]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/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-874/semantics/proofs]0;Holmake: ~/regression-worker/cakeml-874/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-874/translator/monadic]0;Holmake: ~/regression-worker/cakeml-874/characteristic]0;Holmake: ~/regression-worker/cakeml-874/compiler/parsing]0;Holmake: ~/regression-worker/cakeml-874/compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ~/regression-worker/cakeml-874/characteristic]0;Holmake: ~/regression-worker/cakeml-874/translator]0;Holmake: ~/regression-worker/cakeml-874/translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ~/regression-worker/cakeml-874/characteristic]0;Holmake: ~/regression-worker/cakeml-874/characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: ~/regression-worker/cakeml-874/translator/monadic]0;Holmake: ~/regression-worker/cakeml-874/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
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
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
stack_namesProofTheory                                                       OK
Starting work on word_to_stackProofTheory
data_to_word_bignumProofTheory                                               OK
Starting work on data_to_word_assignProofTheory
stack_allocProofTheory                                                       OK
Starting work on word_elimProofTheory
word_elimProofTheory                                                         OK
Starting work on README.md
README.md                                                                    OK
data_to_word_assignProofTheory                                      FAILED! <1>
 t.termdep > 1  do_app op vals x = Rval (v,s2) 
 q r.
     evaluate (FST (assign c n l dest op args names_opt),t) = (q,r) 
     (q = SOME NotEnoughSpace  r.ffi = t.ffi) 
     (q  SOME NotEnoughSpace 
      state_rel c l1 l2 (set_var dest v s2) r [] locs  q = NONE)
 
 failed.
 Failed to prove theorem assign_FP_top.
 Uncaught exception: HOL_ERR {message = " (THEN1 on line 8639)", origin_function = "DISCH_THEN", origin_structure = "Thm_cont"}
flat_to_patProofTheory                                                 M-KILLED
word_to_stackProofTheory                                               M-KILLED