Job 548

CakeML:efa6a90d99c110861c5eb715cb3af0fd6ffeda40
  use existing `disjnt` constant [Oct 30 16:09:59]
HOL:1c953ffcd81a850e2bc8f495591566fab306197d
  Have testutils.die automatically print out "FAILED" [Oct 29 00:48:17]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Oct 30 19:33:50 Claimed job
Oct 30 19:33:55 Reusing HOL
Oct 30 19:34:49 Starting developers/bin
Oct 30 19:36:03 Finished developers/bin                                        1m13s 916MB
Oct 30 19:36:04 Starting semantics/ffi
Oct 30 19:36:16 Finished semantics/ffi                                           11s 247MB
Oct 30 19:36:16 Starting semantics
Oct 30 19:37:33 Finished semantics                                             1m16s 832MB
Oct 30 19:37:34 Starting semantics/proofs
Oct 30 19:40:28 Finished semantics/proofs                                      2m53s   1GB
Oct 30 19:40:28 Starting basis/pure
Oct 30 19:41:20 Finished basis/pure                                              51s 703MB
Oct 30 19:41:21 Starting translator
Oct 30 19:44:26 Finished translator                                            3m04s   1GB
Oct 30 19:44:27 Starting compiler/parsing
Oct 30 19:45:46 Finished compiler/parsing                                      1m18s   2GB
Oct 30 19:45:46 Starting characteristic
Oct 30 19:48:18 Finished characteristic                                        2m31s   1GB
Oct 30 19:48:19 Starting translator/monadic
Oct 30 19:49:45 Finished translator/monadic                                    1m25s   1GB
Oct 30 19:49:45 Starting basis
Oct 30 20:06:40 Finished basis                                                16m53s   2GB
Oct 30 20:06:40 Starting compiler/inference
Oct 30 20:08:05 Finished compiler/inference                                    1m24s   1GB
Oct 30 20:08:06 Starting compiler/backend/reg_alloc
Oct 30 20:08:54 Finished compiler/backend/reg_alloc                              47s   1GB
Oct 30 20:08:54 Starting compiler/backend/gc
Oct 30 20:15:28 Finished compiler/backend/gc                                   6m32s   1GB
Oct 30 20:15:28 Starting compiler/backend
Oct 30 20:15:32 Finished compiler/backend                                         2s  17MB
Oct 30 20:15:32 Starting compiler/encoders/asm
Oct 30 20:15:34 Finished compiler/encoders/asm                                    1s  15MB
Oct 30 20:15:35 Starting compiler/encoders/x64
Oct 30 20:15:51 Finished compiler/encoders/x64                                   15s 424MB
Oct 30 20:15:52 Starting compiler/encoders/arm6
Oct 30 20:16:37 Finished compiler/encoders/arm6                                  44s 405MB
Oct 30 20:16:38 Starting compiler/encoders/arm8
Oct 30 20:16:46 Finished compiler/encoders/arm8                                   7s 342MB
Oct 30 20:16:47 Starting compiler/encoders/mips
Oct 30 20:16:57 Finished compiler/encoders/mips                                   9s 448MB
Oct 30 20:16:58 Starting compiler/encoders/riscv
Oct 30 20:17:06 Finished compiler/encoders/riscv                                  8s 462MB
Oct 30 20:17:07 Starting compiler/backend/x64
Oct 30 20:17:26 Finished compiler/backend/x64                                    17s   1GB
Oct 30 20:17:26 Starting compiler/backend/arm6
Oct 30 20:17:47 Finished compiler/backend/arm6                                   19s   1GB
Oct 30 20:17:47 Starting compiler/backend/arm8
Oct 30 20:18:06 Finished compiler/backend/arm8                                   18s   1GB
Oct 30 20:18:07 Starting compiler/backend/mips
Oct 30 20:18:27 Finished compiler/backend/mips                                   19s   1GB
Oct 30 20:18:28 Starting compiler/backend/riscv
Oct 30 20:18:46 Finished compiler/backend/riscv                                  18s   1GB
Oct 30 20:18:47 Starting compiler/parsing/proofs
Oct 30 20:24:53 Finished compiler/parsing/proofs                               6m05s 809MB
Oct 30 20:24:54 Starting compiler/inference/proofs
Oct 30 20:27:46 Finished compiler/inference/proofs                             2m51s   1GB
Oct 30 20:27:47 Starting compiler/backend/semantics
Oct 30 20:36:55 Finished compiler/backend/semantics                            9m06s   2GB
Oct 30 20:36:55 Starting compiler/backend/reg_alloc/proofs
Oct 30 20:39:47 FAILED: compiler/backend/reg_alloc/proofs
]0;Holmake: ../../../../misc]0;Holmake: ~/oven/regression/HOL-1c953ffcd81a850e2bc8f495591566fab306197d/examples/machine-code/hoare-triple]0;Holmake: ~/oven/regression/HOL-1c953ffcd81a850e2bc8f495591566fab306197d/examples/machine-code/hoare-tripleWorking in $(HOLDIR)/examples/machine-code/hoare-triple
]0;Holmake: ../../../../misc]0;Holmake: ../../../../developers]0;Holmake: ../../../../developersWorking in ../../../../developers
]0;Holmake: ../../../../misc]0;Holmake: ../../../../misc/lem_lib_stub]0;Holmake: ~/oven/regression/HOL-1c953ffcd81a850e2bc8f495591566fab306197d/examples/formal-languages/context-free]0;Holmake: ~/oven/regression/HOL-1c953ffcd81a850e2bc8f495591566fab306197d/examples/formal-languages/context-freeWorking in $(HOLDIR)/examples/formal-languages/context-free
]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: ..]0;Holmake: ../../../../translator/monadic]0;Holmake: ../../../../characteristic]0;Holmake: ../../../../basis/pure]0;Holmake: ~/oven/regression/HOL-1c953ffcd81a850e2bc8f495591566fab306197d/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-1c953ffcd81a850e2bc8f495591566fab306197d/examples/balanced_bst]0;Holmake: ~/oven/regression/HOL-1c953ffcd81a850e2bc8f495591566fab306197d/examples/balanced_bstWorking in $(HOLDIR)/examples/balanced_bst
]0;Holmake: ~/oven/regression/HOL-1c953ffcd81a850e2bc8f495591566fab306197d/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-1c953ffcd81a850e2bc8f495591566fab306197d/examples/formal-languages]0;Holmake: ~/oven/regression/HOL-1c953ffcd81a850e2bc8f495591566fab306197d/examples/formal-languagesWorking in $(HOLDIR)/examples/formal-languages
]0;Holmake: ~/oven/regression/HOL-1c953ffcd81a850e2bc8f495591566fab306197d/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-1c953ffcd81a850e2bc8f495591566fab306197d/examples/formal-languages/regularWorking in $(HOLDIR)/examples/formal-languages/regular
]0;Holmake: ../../../../basis/pure]0;Holmake: ../../../../basis/pureWorking in $(CAKEMLDIR)/basis/pure
]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: ..]0;Holmake: ../../../../unverified/reg_alloc]0;Holmake: ../../../../unverified/reg_allocWorking in $(CAKEMLDIR)/unverified/reg_alloc
]0;Holmake: ..]0;Holmake: ..Working in $(CAKEMLDIR)/compiler/backend/reg_alloc
]0;Holmake: .]0;Holmake: .Working in $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
Starting work on heap
heap                                                                         OK
Starting work on reg_allocProofTheory
reg_allocProofTheory                                                         OK
Starting work on linear_scanProofTheory
linear_scanProofTheory                                              FAILED! <1>
         spill_register (st with active := FILTER ((e,r). r  reg) st.active)
           reg sth 
         good_linear_scan_state int_beg int_end stout sthout (reg::l) pos
           forced mincol  LENGTH sthout.colors = LENGTH sth.colors 
         (r. r  reg  EL r sth.colors = EL r sthout.colors) 
         stout.colormax = st.colormax  st.colormax  EL reg sthout.colors
 
 failed.
 Failed to prove theorem spill_register_FILTER_invariants_hidden.
 Uncaught exception: HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 2618) (THEN1 on line 2619) (THEN1 on line 2620) (THEN1 on line 2621) (THEN1 on line 2622) (THEN1 on line 2623) (THEN1 on line 2624) (THEN1 on line 2625) (THEN1 on line 2634) (THEN1 on line 2635) (THEN1 on line 2636) (THEN1 on line 2640) (THEN1 on line 2655) (THEN1 on line 2656) (THEN1 on line 2661) (THEN1 on line 2662)", origin_function = "THEN1", origin_structure = "Tactical"}