Job 549

CakeML:efa6a90d99c110861c5eb715cb3af0fd6ffeda40
  use existing `disjnt` constant [Oct 30 16:09:59]
HOL:b97e7e9c09f9a3cbc2e810104cffe0c951a1a64d
  Add some subscript Unicode characters (+, -, =) to emacs bindings [Nov 02 06:23:37]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Nov 02 09:24:17 Claimed job
Nov 02 09:25:04 Building HOL
Nov 02 09:34:24 Starting developers/bin
Nov 02 09:35:41 Finished developers/bin                                        1m16s 916MB
Nov 02 09:35:42 Starting semantics/ffi
Nov 02 09:36:21 Finished semantics/ffi                                           38s 632MB
Nov 02 09:36:22 Starting semantics
Nov 02 09:37:49 Finished semantics                                             1m26s 849MB
Nov 02 09:37:49 Starting semantics/proofs
Nov 02 09:40:39 Finished semantics/proofs                                      2m49s   1GB
Nov 02 09:40:40 Starting basis/pure
Nov 02 09:44:20 Finished basis/pure                                            3m38s 614MB
Nov 02 09:44:20 Starting translator
Nov 02 09:47:22 Finished translator                                            3m00s   1GB
Nov 02 09:47:22 Starting compiler/parsing
Nov 02 09:48:37 Finished compiler/parsing                                      1m13s   1GB
Nov 02 09:48:37 Starting characteristic
Nov 02 09:51:06 Finished characteristic                                        2m28s   1GB
Nov 02 09:51:07 Starting translator/monadic
Nov 02 09:52:34 Finished translator/monadic                                    1m26s   1GB
Nov 02 09:52:35 Starting basis
Nov 02 10:09:23 Finished basis                                                16m46s   3GB
Nov 02 10:09:23 Starting compiler/inference
Nov 02 10:11:06 Finished compiler/inference                                    1m41s   1GB
Nov 02 10:11:07 Starting compiler/backend/reg_alloc
Nov 02 10:11:54 Finished compiler/backend/reg_alloc                              47s   1GB
Nov 02 10:11:55 Starting compiler/backend/gc
Nov 02 10:19:16 Finished compiler/backend/gc                                   7m19s   1GB
Nov 02 10:19:16 Starting compiler/backend
Nov 02 10:19:20 Finished compiler/backend                                         3s  21MB
Nov 02 10:19:20 Starting compiler/encoders/asm
Nov 02 10:19:23 Finished compiler/encoders/asm                                    1s  12MB
Nov 02 10:19:23 Starting compiler/encoders/x64
Nov 02 10:20:16 Finished compiler/encoders/x64                                   51s 586MB
Nov 02 10:20:17 Starting compiler/encoders/arm6
Nov 02 10:22:01 Finished compiler/encoders/arm6                                1m43s   1GB
Nov 02 10:22:02 Starting compiler/encoders/arm8
Nov 02 10:22:28 Finished compiler/encoders/arm8                                  25s 485MB
Nov 02 10:22:29 Starting compiler/encoders/mips
Nov 02 10:23:26 Finished compiler/encoders/mips                                  57s 922MB
Nov 02 10:23:27 Starting compiler/encoders/riscv
Nov 02 10:24:28 Finished compiler/encoders/riscv                               1m00s 692MB
Nov 02 10:24:29 Starting compiler/backend/x64
Nov 02 10:24:47 Finished compiler/backend/x64                                    17s 832MB
Nov 02 10:24:47 Starting compiler/backend/arm6
Nov 02 10:25:07 Finished compiler/backend/arm6                                   19s   1GB
Nov 02 10:25:08 Starting compiler/backend/arm8
Nov 02 10:25:27 Finished compiler/backend/arm8                                   17s 893MB
Nov 02 10:25:27 Starting compiler/backend/mips
Nov 02 10:25:47 Finished compiler/backend/mips                                   19s   1GB
Nov 02 10:25:48 Starting compiler/backend/riscv
Nov 02 10:26:08 Finished compiler/backend/riscv                                  18s   1GB
Nov 02 10:26:09 Starting compiler/parsing/proofs
Nov 02 10:32:16 Finished compiler/parsing/proofs                               6m06s   1GB
Nov 02 10:32:17 Starting compiler/inference/proofs
Nov 02 10:35:11 Finished compiler/inference/proofs                             2m53s   1GB
Nov 02 10:35:11 Starting compiler/backend/semantics
Nov 02 10:44:05 Finished compiler/backend/semantics                            8m52s   2GB
Nov 02 10:44:05 Starting compiler/backend/reg_alloc/proofs
Nov 02 10:46:58 FAILED: compiler/backend/reg_alloc/proofs
]0;Holmake: ../../../../misc]0;Holmake: ~/oven/regression/HOL-b97e7e9c09f9a3cbc2e810104cffe0c951a1a64d/examples/machine-code/hoare-triple]0;Holmake: ~/oven/regression/HOL-b97e7e9c09f9a3cbc2e810104cffe0c951a1a64d/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-b97e7e9c09f9a3cbc2e810104cffe0c951a1a64d/examples/formal-languages/context-free]0;Holmake: ~/oven/regression/HOL-b97e7e9c09f9a3cbc2e810104cffe0c951a1a64d/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-b97e7e9c09f9a3cbc2e810104cffe0c951a1a64d/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-b97e7e9c09f9a3cbc2e810104cffe0c951a1a64d/examples/balanced_bst]0;Holmake: ~/oven/regression/HOL-b97e7e9c09f9a3cbc2e810104cffe0c951a1a64d/examples/balanced_bstWorking in $(HOLDIR)/examples/balanced_bst
]0;Holmake: ~/oven/regression/HOL-b97e7e9c09f9a3cbc2e810104cffe0c951a1a64d/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-b97e7e9c09f9a3cbc2e810104cffe0c951a1a64d/examples/formal-languages]0;Holmake: ~/oven/regression/HOL-b97e7e9c09f9a3cbc2e810104cffe0c951a1a64d/examples/formal-languagesWorking in $(HOLDIR)/examples/formal-languages
]0;Holmake: ~/oven/regression/HOL-b97e7e9c09f9a3cbc2e810104cffe0c951a1a64d/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-b97e7e9c09f9a3cbc2e810104cffe0c951a1a64d/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"}