Job 793

CakeML:84be3269450a8eb815bcc20e0dd686f66ca21fea
  Update backendComputeLib use of ThmSetData. [Apr 12 13:44:08]
#630 (compute-thmset)
Merging into:4c7ed00f29e1d06e8f4b0e919d49d0c3398a4824
  Fix a number of saves of definitions that cause loss of "compute" [Apr 14 12:49:44]
HOL:a083c115f48c74233904c5c3e8fa848239e6ab9c
  Deal with rebindings of ptree_{size,fringe}_def in grammarScript [Apr 13 11:02:48]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Apr 14 16:35:04 Claimed job
Apr 14 16:35:09 Reusing HOL
Apr 14 16:36:02 Starting developers
Apr 14 16:36:04 Finished developers                                               2s  20MB
Apr 14 16:36:05 Starting developers/bin
Apr 14 16:37:15 Finished developers/bin                                        1m09s 918MB
Apr 14 16:37:15 Starting semantics/ffi
Apr 14 16:37:25 Finished semantics/ffi                                            9s 234MB
Apr 14 16:37:26 Starting semantics
Apr 14 16:38:48 Finished semantics                                             1m22s   1GB
Apr 14 16:38:48 Starting semantics/proofs
Apr 14 16:41:43 Finished semantics/proofs                                      2m54s 977MB
Apr 14 16:41:43 Starting basis/pure
Apr 14 16:42:31 Finished basis/pure                                              47s 656MB
Apr 14 16:42:31 Starting translator
Apr 14 16:44:12 Finished translator                                            1m40s   1GB
Apr 14 16:44:13 Starting compiler/parsing
Apr 14 16:45:10 Finished compiler/parsing                                        56s   1GB
Apr 14 16:45:10 Starting characteristic
Apr 14 16:50:25 Finished characteristic                                        5m14s   1GB
Apr 14 16:50:25 Starting translator/monadic
Apr 14 16:51:55 Finished translator/monadic                                    1m29s   1GB
Apr 14 16:51:55 Starting basis
Apr 14 17:08:33 Finished basis                                                16m37s   2GB
Apr 14 17:08:33 Starting compiler/inference
Apr 14 17:10:05 Finished compiler/inference                                    1m31s   1GB
Apr 14 17:10:05 Starting compiler/backend/reg_alloc
Apr 14 17:10:58 Finished compiler/backend/reg_alloc                              52s   1GB
Apr 14 17:10:58 Starting compiler/backend/gc
Apr 14 17:18:57 Finished compiler/backend/gc                                   7m58s   1GB
Apr 14 17:18:57 Starting compiler/backend
Apr 14 17:19:00 Finished compiler/backend                                         2s  20MB
Apr 14 17:19:00 Starting compiler/encoders/asm
Apr 14 17:19:02 Finished compiler/encoders/asm                                    1s  18MB
Apr 14 17:19:02 Starting compiler/encoders/x64
Apr 14 17:19:27 Finished compiler/encoders/x64                                   25s 944MB
Apr 14 17:19:28 Starting compiler/encoders/arm6
Apr 14 17:20:13 Finished compiler/encoders/arm6                                  44s 684MB
Apr 14 17:20:13 Starting compiler/encoders/arm8
Apr 14 17:20:27 Finished compiler/encoders/arm8                                  13s 845MB
Apr 14 17:20:27 Starting compiler/encoders/mips
Apr 14 17:20:45 Finished compiler/encoders/mips                                  17s 761MB
Apr 14 17:20:45 Starting compiler/encoders/riscv
Apr 14 17:21:00 Finished compiler/encoders/riscv                                 14s 782MB
Apr 14 17:21:01 Starting compiler/encoders/ag32
Apr 14 17:21:18 Finished compiler/encoders/ag32                                  17s 749MB
Apr 14 17:21:18 Starting compiler/backend/x64
Apr 14 17:21:35 Finished compiler/backend/x64                                    17s 841MB
Apr 14 17:21:36 Starting compiler/backend/arm6
Apr 14 17:21:56 Finished compiler/backend/arm6                                   20s   1GB
Apr 14 17:21:57 Starting compiler/backend/arm8
Apr 14 17:22:15 Finished compiler/backend/arm8                                   17s 944MB
Apr 14 17:22:15 Starting compiler/backend/mips
Apr 14 17:22:35 Finished compiler/backend/mips                                   19s   1GB
Apr 14 17:22:35 Starting compiler/backend/riscv
Apr 14 17:22:54 Finished compiler/backend/riscv                                  19s   1GB
Apr 14 17:22:55 Starting compiler/backend/ag32
Apr 14 17:24:02 Finished compiler/backend/ag32                                 1m07s   1GB
Apr 14 17:24:03 Starting compiler/parsing/proofs
Apr 14 17:29:38 Finished compiler/parsing/proofs                               5m35s   1GB
Apr 14 17:29:39 Starting compiler/inference/proofs
Apr 14 17:32:19 Finished compiler/inference/proofs                             2m40s   1GB
Apr 14 17:32:19 Starting compiler/backend/semantics
Apr 14 17:39:12 Finished compiler/backend/semantics                            6m52s   1GB
Apr 14 17:39:13 Starting compiler/backend/reg_alloc/proofs
Apr 14 17:41:49 Finished compiler/backend/reg_alloc/proofs                     2m36s 805MB
Apr 14 17:41:49 Starting compiler/backend/proofs
Apr 14 17:43:05 FAILED: compiler/backend/proofs
]0;Holmake: .]0;Holmake: ~/oven/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/machine-code/multiword]0;Holmake: ~/oven/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/machine-code/multiwordWorking in $(HOLDIR)/examples/machine-code/multiword
]0;Holmake: .]0;Holmake: ..]0;Holmake: ~/oven/regression/cakeml-793/basis/pure]0;Holmake: ~/oven/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/balanced_bst]0;Holmake: ~/oven/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/balanced_bstWorking in $(HOLDIR)/examples/balanced_bst
]0;Holmake: ~/oven/regression/cakeml-793/basis/pure]0;Holmake: ~/oven/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/formal-languages]0;Holmake: ~/oven/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/formal-languagesWorking in $(HOLDIR)/examples/formal-languages
]0;Holmake: ~/oven/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/formal-languages/context-free]0;Holmake: ~/oven/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/formal-languages/context-freeWorking in $(HOLDIR)/examples/formal-languages/context-free
]0;Holmake: ~/oven/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/formal-languages/regularWorking in $(HOLDIR)/examples/formal-languages/regular
]0;Holmake: ~/oven/regression/cakeml-793/basis/pure]0;Holmake: ~/oven/regression/cakeml-793/misc]0;Holmake: ~/oven/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/oven/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: ~/oven/regression/cakeml-793/misc]0;Holmake: ~/oven/regression/cakeml-793/developers]0;Holmake: ~/oven/regression/cakeml-793/developersWorking in $(CAKEMLDIR)/developers
]0;Holmake: ~/oven/regression/cakeml-793/misc]0;Holmake: ~/oven/regression/cakeml-793/misc/lem_lib_stub]0;Holmake: ~/oven/regression/cakeml-793/misc/lem_lib_stubWorking in $(CAKEMLDIR)/misc/lem_lib_stub
]0;Holmake: ~/oven/regression/cakeml-793/misc]0;Holmake: ~/oven/regression/cakeml-793/miscWorking in $(CAKEMLDIR)/misc
]0;Holmake: ~/oven/regression/cakeml-793/basis/pure]0;Holmake: ~/oven/regression/cakeml-793/basis/pureWorking in $(CAKEMLDIR)/basis/pure
]0;Holmake: ..]0;Holmake: ../reg_alloc]0;Holmake: ~/oven/regression/cakeml-793/translator/monadic/monad_base]0;Holmake: ~/oven/regression/cakeml-793/semantics]0;Holmake: ~/oven/regression/cakeml-793/semantics/ffi]0;Holmake: ~/oven/regression/cakeml-793/semantics/ffiWorking in $(CAKEMLDIR)/semantics/ffi
]0;Holmake: ~/oven/regression/cakeml-793/semantics]0;Holmake: ~/oven/regression/cakeml-793/semanticsWorking in $(CAKEMLDIR)/semantics
]0;Holmake: ~/oven/regression/cakeml-793/translator/monadic/monad_base]0;Holmake: ~/oven/regression/cakeml-793/translator/monadic/monad_baseWorking in $(CAKEMLDIR)/translator/monadic/monad_base
]0;Holmake: ../reg_alloc]0;Holmake: ~/oven/regression/cakeml-793/unverified/reg_alloc]0;Holmake: ~/oven/regression/cakeml-793/unverified/reg_allocWorking in $(CAKEMLDIR)/unverified/reg_alloc
]0;Holmake: ../reg_alloc]0;Holmake: ../reg_allocWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc
]0;Holmake: ..]0;Holmake: ../../encoders/asm]0;Holmake: ~/oven/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/l3-machine-code/common]0;Holmake: ~/oven/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/l3-machine-code/commonWorking in $(HOLDIR)/examples/l3-machine-code/common
]0;Holmake: ../../encoders/asm]0;Holmake: ../../encoders/asmWorking in $(CAKEMLDIR)/compiler/encoders/asm
]0;Holmake: ..]0;Holmake: ~/oven/regression/cakeml-793/semantics/proofs]0;Holmake: ~/oven/regression/cakeml-793/semantics/proofsWorking in $(CAKEMLDIR)/semantics/proofs
]0;Holmake: ..]0;Holmake: ..Working in $(CAKEMLDIR)/compiler/backend
]0;Holmake: .]0;Holmake: ../gc]0;Holmake: ../gcWorking in $(CAKEMLDIR)/compiler/backend/gc
]0;Holmake: .]0;Holmake: ../reg_alloc/proofs]0;Holmake: ~/oven/regression/cakeml-793/translator/monadic]0;Holmake: ~/oven/regression/cakeml-793/characteristic]0;Holmake: ~/oven/regression/cakeml-793/compiler/parsing]0;Holmake: ~/oven/regression/cakeml-793/compiler/parsingWorking in $(CAKEMLDIR)/compiler/parsing
]0;Holmake: ~/oven/regression/cakeml-793/characteristic]0;Holmake: ~/oven/regression/cakeml-793/translator]0;Holmake: ~/oven/regression/cakeml-793/translatorWorking in $(CAKEMLDIR)/translator
]0;Holmake: ~/oven/regression/cakeml-793/characteristic]0;Holmake: ~/oven/regression/cakeml-793/characteristicWorking in $(CAKEMLDIR)/characteristic
]0;Holmake: ~/oven/regression/cakeml-793/translator/monadic]0;Holmake: ~/oven/regression/cakeml-793/translator/monadicWorking in $(CAKEMLDIR)/translator/monadic
]0;Holmake: ../reg_alloc/proofs]0;Holmake: ../reg_alloc/proofsWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
]0;Holmake: .]0;Holmake: ../semantics]0;Holmake: ../semanticsWorking in $(CAKEMLDIR)/compiler/backend/semantics
]0;Holmake: .]0;Holmake: .Working in $(CAKEMLDIR)/compiler/backend/proofs
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                                            FAILED! <1>
 error in quse /home/cake/oven/regression/cakeml-793/compiler/backend/proofs/clos_annotateProofScript.sml : HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 1322)", origin_function = "THEN1", origin_structure = "Tactical"}
 error in load clos_annotateProofScript : HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 1322)", origin_function = "THEN1", origin_structure = "Tactical"}
 Proof of 
 
 xs m l i.
     EVERY (obeys_max_app n) xs  EVERY (obeys_max_app n) (FST (alt_free xs))
 
 failed.
 Failed to prove theorem alt_free_obeys_max_app.
 Uncaught exception: HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 1322)", origin_function = "THEN1", origin_structure = "Tactical"}
bvi_tailrecProofTheory                                                 M-KILLED
bvi_to_dataProofTheory                                                 M-KILLED
bvl_handleProofTheory                                                  M-KILLED