Job 1238

CakeML:df6040d0801a1f5c6322a43858733b97daaa3b3b
  Fix a broken proof [May 29 19:34:44]
HOL:16a774456e43bd29a9b94ee31e24f17e059e771f
  Implement a unification-based version of mp_then with similar API [May 20 07:12:37]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

May 30 13:00:01 Claimed job
May 30 13:00:03 Reusing HOL
May 30 13:00:49 Starting developers
May 30 13:00:54 Finished developers                                               4s  93MB
May 30 13:00:54 Starting developers/bin
May 30 13:01:01 Finished developers/bin                                           7s   1GB
May 30 13:01:02 Starting semantics/ffi
May 30 13:01:12 Finished semantics/ffi                                           10s 223MB
May 30 13:01:12 Starting semantics
May 30 13:02:35 Finished semantics                                             1m22s   1GB
May 30 13:02:35 Starting semantics/proofs
May 30 13:06:06 Finished semantics/proofs                                      3m30s   1GB
May 30 13:06:06 Starting semantics/alt_semantics
May 30 13:06:14 Finished semantics/alt_semantics                                  8s 289MB
May 30 13:06:15 Starting semantics/alt_semantics/proofs
May 30 13:08:28 Finished semantics/alt_semantics/proofs                        2m13s 792MB
May 30 13:08:28 Starting basis/pure
May 30 13:09:19 Finished basis/pure                                              50s 897MB
May 30 13:09:19 Starting translator
May 30 13:12:00 Finished translator                                            2m40s   1GB
May 30 13:12:00 Starting compiler/parsing
May 30 13:13:12 Finished compiler/parsing                                      1m12s   2GB
May 30 13:13:12 Starting characteristic
May 30 13:19:18 Finished characteristic                                        6m05s   1GB
May 30 13:19:18 Starting translator/monadic
May 30 13:20:56 Finished translator/monadic                                    1m37s   1GB
May 30 13:20:56 Starting basis
May 30 13:54:23 Finished basis                                                33m26s  10GB
May 30 13:54:23 Starting compiler/inference
May 30 13:55:24 Finished compiler/inference                                    1m00s   1GB
May 30 13:55:25 Starting compiler/backend/reg_alloc
May 30 13:56:29 Finished compiler/backend/reg_alloc                            1m04s   1GB
May 30 13:56:29 Starting compiler/backend/gc
May 30 13:59:49 Finished compiler/backend/gc                                   3m19s   1GB
May 30 13:59:49 Starting compiler/backend
May 30 14:04:33 Finished compiler/backend                                      4m43s   2GB
May 30 14:04:33 Starting compiler/encoders/asm
May 30 14:04:55 Finished compiler/encoders/asm                                   22s 829MB
May 30 14:04:55 Starting compiler/encoders/x64
May 30 14:05:21 Finished compiler/encoders/x64                                   25s 837MB
May 30 14:05:21 Starting compiler/encoders/arm7
May 30 14:06:11 Finished compiler/encoders/arm7                                  50s 770MB
May 30 14:06:12 Starting compiler/encoders/arm8
May 30 14:06:26 Finished compiler/encoders/arm8                                  13s 648MB
May 30 14:06:26 Starting compiler/encoders/mips
May 30 14:06:44 Finished compiler/encoders/mips                                  17s   1GB
May 30 14:06:44 Starting compiler/encoders/riscv
May 30 14:06:59 Finished compiler/encoders/riscv                                 15s   1GB
May 30 14:06:59 Starting compiler/encoders/ag32
May 30 14:07:18 Finished compiler/encoders/ag32                                  18s 603MB
May 30 14:07:18 Starting compiler/backend/x64
May 30 14:07:37 Finished compiler/backend/x64                                    18s   1GB
May 30 14:07:37 Starting compiler/backend/arm7
May 30 14:07:58 Finished compiler/backend/arm7                                   20s   1GB
May 30 14:07:58 Starting compiler/backend/arm8
May 30 14:08:17 Finished compiler/backend/arm8                                   19s   1GB
May 30 14:08:17 Starting compiler/backend/mips
May 30 14:08:37 Finished compiler/backend/mips                                   19s   1GB
May 30 14:08:37 Starting compiler/backend/riscv
May 30 14:08:57 Finished compiler/backend/riscv                                  19s   1GB
May 30 14:08:57 Starting compiler/backend/ag32
May 30 14:10:10 Finished compiler/backend/ag32                                 1m13s   1GB
May 30 14:10:11 Starting compiler/parsing/proofs
May 30 14:16:00 Finished compiler/parsing/proofs                               5m49s   1GB
May 30 14:16:01 Starting compiler/inference/proofs
May 30 14:18:34 Finished compiler/inference/proofs                             2m33s   1GB
May 30 14:18:34 Starting compiler/backend/semantics
May 30 14:49:28 Finished compiler/backend/semantics                           30m53s   2GB
May 30 14:49:28 Starting compiler/backend/reg_alloc/proofs
May 30 14:53:10 Finished compiler/backend/reg_alloc/proofs                     3m41s   1GB
May 30 14:53:10 Starting compiler/backend/proofs
May 30 15:38:27 FAILED: compiler/backend/proofs
Scanning $(HOLDIR)/examples/machine-code/multiword
Scanning $(HOLDIR)/examples/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc/lem_lib_stub
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/compiler/backend/pattern_matching
Scanning $(CAKEMLDIR)/compiler/backend/reachability
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/unverified/reg_alloc
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc
Scanning $(HOLDIR)/examples/l3-machine-code/common
Scanning $(CAKEMLDIR)/compiler/encoders/asm
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/compiler/backend
Scanning $(CAKEMLDIR)/compiler/backend/gc
Scanning $(CAKEMLDIR)/compiler/backend/reachability/proofs
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/characteristic
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
Scanning $(CAKEMLDIR)/compiler/backend/semantics
Starting work on reachable_sptProofTheory
Starting work on README.md
Starting work on bvi_tailrecProofTheory
Starting work on data_liveProofTheory
README.md                                       real:    1s  user:    0s     OK
Starting work on data_simpProofTheory
reachable_sptProofTheory                        real:   12s  user:   11s     OK
Starting work on data_spaceProofTheory
data_simpProofTheory                            real:   15s  user:   14s     OK
Starting work on bvl_constProofTheory
data_spaceProofTheory                           real:   28s  user:   26s     OK
Starting work on bvi_letProofTheory
bvi_letProofTheory                              real:   19s  user:   18s     OK
Starting work on clos_annotateProofTheory
bvl_constProofTheory                            real:   53s  user:   52s     OK
Starting work on bvl_handleProofTheory
data_liveProofTheory                            real:   75s  user:   73s     OK
Starting work on bvi_to_dataProofTheory
clos_annotateProofTheory                        real:   28s  user:   26s     OK
Starting work on clos_callProofTheory
bvl_handleProofTheory                           real:   21s  user:   20s     OK
Starting work on bvl_inlineProofTheory
bvl_inlineProofTheory                           real:   34s  user:   33s     OK
Starting work on clos_fvsProofTheory
clos_fvsProofTheory                             real:   19s  user:   18s     OK
Starting work on clos_knownPropsTheory
clos_knownPropsTheory                           real:   11s  user:   10s     OK
Starting work on clos_letopProofTheory
clos_letopProofTheory                           real:   19s  user:   18s     OK
Starting work on clos_ticksProofTheory
bvi_tailrecProofTheory                          real:  194s  user:  191s     OK
Starting work on bvl_to_bviProofTheory
clos_ticksProofTheory                           real:   26s  user:   24s     OK
Starting work on clos_knownProofTheory
bvi_to_dataProofTheory                          real:  141s  user:  137s     OK
Starting work on clos_mtiProofTheory
clos_mtiProofTheory                             real:   37s  user:   35s     OK
Starting work on clos_numberProofTheory
clos_callProofTheory                            real:  185s  user:  181s     OK
Starting work on bvl_jumpProofTheory
clos_numberProofTheory                          real:   27s  user:   26s     OK
Starting work on word_simpProofTheory
bvl_jumpProofTheory                             real:   10s  user:    9s     OK
Starting work on word_bignumProofTheory
clos_knownProofTheory                           real:  134s  user:  131s     OK
Starting work on clos_to_bvlProofTheory
word_simpProofTheory                            real:   55s  user:   54s     OK
Starting work on word_gcFunctionsTheory
word_gcFunctionsTheory                          real:   27s  user:   26s     OK
Starting work on data_to_word_memoryProofTheory
bvl_to_bviProofTheory                           real:  200s  user:  196s     OK
Starting work on word_allocProofTheory
word_bignumProofTheory                          real:  216s  user:  212s     OK
Starting work on word_instProofTheory
word_instProofTheory                            real:   53s  user:   51s     OK
Starting work on word_removeProofTheory
clos_to_bvlProofTheory                          real:  219s  user:  214s     OK
Starting work on word_depthProofTheory
word_removeProofTheory                          real:   30s  user:   29s     OK
Starting work on flat_patternProofTheory
word_depthProofTheory                           real:   72s  user:   70s     OK
Starting work on flat_to_closProofTheory
flat_patternProofTheory                         real:   50s  user:   48s     OK
Starting work on lab_filterProofTheory
flat_to_closProofTheory                         real:   59s  user:   57s     OK
Starting work on stack_removeProofTheory
lab_filterProofTheory                           real:   60s  user:   58s     OK
Starting work on flat_elimProofTheory
flat_elimProofTheory                            real:   68s  user:   66s     OK
Starting work on source_to_flatProofTheory
source_to_flatProofTheory                       real:  109s  user:  107s     OK
Starting work on stack_allocProofTheory
stack_removeProofTheory                         real:  274s  user:  270s     OK
Starting work on lab_to_targetProofTheory
word_allocProofTheory                           real:  642s  user:  635s     OK
Starting work on word_to_wordProofTheory
word_to_wordProofTheory                         real:   69s  user:   67s     OK
Starting work on stack_namesProofTheory
data_to_word_memoryProofTheory                  real:  747s  user:  740s     OK
Starting work on data_to_word_gcProofTheory
stack_namesProofTheory                          real:   32s  user:   31s     OK
Starting work on stack_rawcallProofTheory
lab_to_targetProofTheory                        real:  238s  user:  235s     OK
Starting work on word_to_stackProofTheory
stack_rawcallProofTheory                        real:   71s  user:   69s     OK
Starting work on word_elimProofTheory
stack_allocProofTheory                          real:  443s  user:  436s     OK
word_elimProofTheory                            real:  129s  user:  127s     OK
data_to_word_gcProofTheory                      real:  253s  user:  248s     OK
Starting work on data_to_word_bignumProofTheory
data_to_word_bignumProofTheory                  real:  274s  user:  271s     OK
Starting work on data_to_word_assignProofTheory
data_to_word_assignProofTheory                  real: 1073s  user: 1064sFAIL<1>
     evaluate (FST (assign c n l dest op args names_opt),t) = (q,r) 
     (q = SOME NotEnoughSpace 
      r.ffi = t.ffi  option_le r.stack_max s2.stack_max 
      (c.gc_kind  None  ~s2.safe_for_space)) 
     (q  SOME NotEnoughSpace 
      state_rel c l1 l2 (set_var dest v s2) r [] locs  q = NONE)
 
 failed.
 Failed to prove theorem assign_WordOpW64.
 Uncaught exception: HOL_ERR {message = "goal completely solved by first tactic (THEN1 on line 10035) (THEN1 on line 10025) (THEN1 on line 10069) (THEN1 on line 10074) (THEN1 on line 10023) (THEN1 on line 10081) (THEN1 on line 10125)", origin_function = "THEN1", origin_structure = "Tactical"}
word_to_stackProofTheory                                                M-KILLED