Job 547

CakeML:33e99acd8473d0f3b26811cff129818bb6b04743
  Merge pull request #545 from CakeML/explorer [Oct 21 01:02:30]
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 10:30:02 Claimed job
Oct 30 10:30:57 Building HOL
Oct 30 10:40:35 Starting developers/bin
Oct 30 10:42:02 Finished developers/bin                                        1m24s 908MB
Oct 30 10:42:03 Starting semantics/ffi
Oct 30 10:43:10 Finished semantics/ffi                                         1m06s 185MB
Oct 30 10:43:11 Starting semantics
Oct 30 10:45:39 Finished semantics                                             2m27s 352MB
Oct 30 10:45:40 Starting semantics/proofs
Oct 30 10:49:16 Finished semantics/proofs                                      3m35s 320MB
Oct 30 10:49:17 Starting basis/pure
Oct 30 10:53:11 Finished basis/pure                                            3m53s 735MB
Oct 30 10:53:11 Starting translator
Oct 30 10:56:19 Finished translator                                            3m06s   1GB
Oct 30 10:56:19 Starting compiler/parsing
Oct 30 10:57:40 Finished compiler/parsing                                      1m19s   1GB
Oct 30 10:57:40 Starting characteristic
Oct 30 11:00:10 Finished characteristic                                        2m28s   1GB
Oct 30 11:00:10 Starting translator/monadic
Oct 30 11:01:39 Finished translator/monadic                                    1m27s   1GB
Oct 30 11:01:39 Starting basis
Oct 30 11:18:43 Finished basis                                                17m02s   3GB
Oct 30 11:18:43 Starting compiler/inference
Oct 30 11:20:26 Finished compiler/inference                                    1m42s   1GB
Oct 30 11:20:27 Starting compiler/backend/reg_alloc
Oct 30 11:21:15 Finished compiler/backend/reg_alloc                              47s 850MB
Oct 30 11:21:16 Starting compiler/backend/gc
Oct 30 11:28:56 Finished compiler/backend/gc                                   7m39s   1GB
Oct 30 11:28:57 Starting compiler/backend
Oct 30 11:29:00 Finished compiler/backend                                         2s  17MB
Oct 30 11:29:01 Starting compiler/encoders/asm
Oct 30 11:29:03 Finished compiler/encoders/asm                                    1s  12MB
Oct 30 11:29:03 Starting compiler/encoders/x64
Oct 30 11:29:55 Finished compiler/encoders/x64                                   51s 580MB
Oct 30 11:29:56 Starting compiler/encoders/arm6
Oct 30 11:31:41 Finished compiler/encoders/arm6                                1m44s   1GB
Oct 30 11:31:42 Starting compiler/encoders/arm8
Oct 30 11:32:08 Finished compiler/encoders/arm8                                  25s 460MB
Oct 30 11:32:09 Starting compiler/encoders/mips
Oct 30 11:33:08 Finished compiler/encoders/mips                                  58s 834MB
Oct 30 11:33:09 Starting compiler/encoders/riscv
Oct 30 11:34:10 Finished compiler/encoders/riscv                               1m00s 693MB
Oct 30 11:34:11 Starting compiler/backend/x64
Oct 30 11:34:29 Finished compiler/backend/x64                                    17s 934MB
Oct 30 11:34:30 Starting compiler/backend/arm6
Oct 30 11:34:50 Finished compiler/backend/arm6                                   19s   1GB
Oct 30 11:34:51 Starting compiler/backend/arm8
Oct 30 11:35:09 Finished compiler/backend/arm8                                   17s 898MB
Oct 30 11:35:10 Starting compiler/backend/mips
Oct 30 11:35:30 Finished compiler/backend/mips                                   19s   1GB
Oct 30 11:35:31 Starting compiler/backend/riscv
Oct 30 11:35:50 Finished compiler/backend/riscv                                  18s   1GB
Oct 30 11:35:50 Starting compiler/parsing/proofs
Oct 30 11:42:00 Finished compiler/parsing/proofs                               6m09s   1GB
Oct 30 11:42:01 Starting compiler/inference/proofs
Oct 30 11:44:53 Finished compiler/inference/proofs                             2m51s   1GB
Oct 30 11:44:54 Starting compiler/backend/semantics
Oct 30 11:54:00 Finished compiler/backend/semantics                            9m04s   2GB
Oct 30 11:54:00 Starting compiler/backend/reg_alloc/proofs
Oct 30 11:56:51 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"}