Job 792

CakeML:40c1eafd0929ce75b9f7ef115bc0a9489983c3fc
  Rename forgotten IOStream to Ustream [Apr 12 16:07:32]
#629 (vstte18)
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:oven2 4.15.0-34-generic x86_64 GNU/Linux

Apr 14 16:22:51 Claimed job
Apr 14 16:22:55 Reusing HOL
Apr 14 16:23:00 Starting developers
Apr 14 16:23:01 Finished developers                                               0s  22MB
Apr 14 16:23:01 Starting developers/bin
Apr 14 16:23:33 Finished developers/bin                                          31s 205MB
Apr 14 16:23:33 Starting semantics/ffi
Apr 14 16:23:41 Finished semantics/ffi                                            7s 222MB
Apr 14 16:23:42 Starting semantics
Apr 14 16:25:01 Finished semantics                                             1m18s   1GB
Apr 14 16:25:01 Starting semantics/proofs
Apr 14 16:27:58 Finished semantics/proofs                                      2m56s   1GB
Apr 14 16:27:58 Starting basis/pure
Apr 14 16:28:43 Finished basis/pure                                              44s 666MB
Apr 14 16:28:43 Starting translator
Apr 14 16:30:24 Finished translator                                            1m40s   1GB
Apr 14 16:30:24 Starting compiler/parsing
Apr 14 16:31:23 Finished compiler/parsing                                        57s   1GB
Apr 14 16:31:23 Starting characteristic
Apr 14 16:36:36 Finished characteristic                                        5m12s   1GB
Apr 14 16:36:36 Starting translator/monadic
Apr 14 16:38:01 Finished translator/monadic                                    1m24s   1GB
Apr 14 16:38:02 Starting basis
Apr 14 16:55:02 Finished basis                                                16m59s   2GB
Apr 14 16:55:02 Starting compiler/inference
Apr 14 16:56:33 Finished compiler/inference                                    1m30s   1GB
Apr 14 16:56:34 Starting compiler/backend/reg_alloc
Apr 14 16:57:25 Finished compiler/backend/reg_alloc                              51s   1GB
Apr 14 16:57:26 Starting compiler/backend/gc
Apr 14 17:05:27 Finished compiler/backend/gc                                   8m01s   2GB
Apr 14 17:05:28 Starting compiler/backend
Apr 14 17:05:29 Finished compiler/backend                                         0s  42MB
Apr 14 17:05:29 Starting compiler/encoders/asm
Apr 14 17:05:30 Finished compiler/encoders/asm                                    0s  32MB
Apr 14 17:05:30 Starting compiler/encoders/x64
Apr 14 17:05:54 Finished compiler/encoders/x64                                   23s 668MB
Apr 14 17:05:54 Starting compiler/encoders/arm6
Apr 14 17:06:39 Finished compiler/encoders/arm6                                  44s 913MB
Apr 14 17:06:39 Starting compiler/encoders/arm8
Apr 14 17:06:51 Finished compiler/encoders/arm8                                  11s 878MB
Apr 14 17:06:51 Starting compiler/encoders/mips
Apr 14 17:07:08 Finished compiler/encoders/mips                                  15s   1GB
Apr 14 17:07:08 Starting compiler/encoders/riscv
Apr 14 17:07:21 Finished compiler/encoders/riscv                                 12s 736MB
Apr 14 17:07:22 Starting compiler/encoders/ag32
Apr 14 17:07:37 Finished compiler/encoders/ag32                                  15s 765MB
Apr 14 17:07:38 Starting compiler/backend/x64
Apr 14 17:07:53 Finished compiler/backend/x64                                    15s   1GB
Apr 14 17:07:53 Starting compiler/backend/arm6
Apr 14 17:08:12 Finished compiler/backend/arm6                                   18s   1GB
Apr 14 17:08:12 Starting compiler/backend/arm8
Apr 14 17:08:28 Finished compiler/backend/arm8                                   15s   1GB
Apr 14 17:08:29 Starting compiler/backend/mips
Apr 14 17:08:45 Finished compiler/backend/mips                                   15s   1GB
Apr 14 17:08:46 Starting compiler/backend/riscv
Apr 14 17:09:02 Finished compiler/backend/riscv                                  16s   1GB
Apr 14 17:09:02 Starting compiler/backend/ag32
Apr 14 17:10:11 Finished compiler/backend/ag32                                 1m08s 960MB
Apr 14 17:10:12 Starting compiler/parsing/proofs
Apr 14 17:15:47 Finished compiler/parsing/proofs                               5m34s 814MB
Apr 14 17:15:47 Starting compiler/inference/proofs
Apr 14 17:18:28 Finished compiler/inference/proofs                             2m40s   1GB
Apr 14 17:18:28 Starting compiler/backend/semantics
Apr 14 17:25:40 Finished compiler/backend/semantics                            7m10s   1GB
Apr 14 17:25:40 Starting compiler/backend/reg_alloc/proofs
Apr 14 17:28:19 Finished compiler/backend/reg_alloc/proofs                     2m39s 699MB
Apr 14 17:28:20 Starting compiler/backend/proofs
Apr 14 17:29:36 FAILED: compiler/backend/proofs
]0;Holmake: .]0;Holmake: ~/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/machine-code/multiword]0;Holmake: ~/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/machine-code/multiword[1mWorking in $(HOLDIR)/examples/machine-code/multiword[0m
]0;Holmake: .]0;Holmake: ..]0;Holmake: ~/regression/cakeml-792/basis/pure]0;Holmake: ~/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/balanced_bst]0;Holmake: ~/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/balanced_bst[1mWorking in $(HOLDIR)/examples/balanced_bst[0m
]0;Holmake: ~/regression/cakeml-792/basis/pure]0;Holmake: ~/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/formal-languages]0;Holmake: ~/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ~/regression/cakeml-792/basis/pure]0;Holmake: ~/regression/cakeml-792/misc]0;Holmake: ~/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/regression/cakeml-792/misc]0;Holmake: ~/regression/cakeml-792/developers]0;Holmake: ~/regression/cakeml-792/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-792/misc]0;Holmake: ~/regression/cakeml-792/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-792/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-792/misc]0;Holmake: ~/regression/cakeml-792/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ~/regression/cakeml-792/basis/pure]0;Holmake: ~/regression/cakeml-792/basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ..]0;Holmake: ../reg_alloc]0;Holmake: ~/regression/cakeml-792/translator/monadic/monad_base]0;Holmake: ~/regression/cakeml-792/semantics]0;Holmake: ~/regression/cakeml-792/semantics/ffi]0;Holmake: ~/regression/cakeml-792/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression/cakeml-792/semantics]0;Holmake: ~/regression/cakeml-792/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ~/regression/cakeml-792/translator/monadic/monad_base]0;Holmake: ~/regression/cakeml-792/translator/monadic/monad_base[1mWorking in $(CAKEMLDIR)/translator/monadic/monad_base[0m
]0;Holmake: ../reg_alloc]0;Holmake: ~/regression/cakeml-792/unverified/reg_alloc]0;Holmake: ~/regression/cakeml-792/unverified/reg_alloc[1mWorking in $(CAKEMLDIR)/unverified/reg_alloc[0m
]0;Holmake: ../reg_alloc]0;Holmake: ../reg_alloc[1mWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc[0m
]0;Holmake: ..]0;Holmake: ../../encoders/asm]0;Holmake: ~/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/l3-machine-code/common]0;Holmake: ~/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/l3-machine-code/common[1mWorking in $(HOLDIR)/examples/l3-machine-code/common[0m
]0;Holmake: ../../encoders/asm]0;Holmake: ../../encoders/asm[1mWorking in $(CAKEMLDIR)/compiler/encoders/asm[0m
]0;Holmake: ..]0;Holmake: ~/regression/cakeml-792/semantics/proofs]0;Holmake: ~/regression/cakeml-792/semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ..]0;Holmake: ..[1mWorking in $(CAKEMLDIR)/compiler/backend[0m
]0;Holmake: .]0;Holmake: ../gc]0;Holmake: ../gc[1mWorking in $(CAKEMLDIR)/compiler/backend/gc[0m
]0;Holmake: .]0;Holmake: ../reg_alloc/proofs]0;Holmake: ~/regression/cakeml-792/translator/monadic]0;Holmake: ~/regression/cakeml-792/characteristic]0;Holmake: ~/regression/cakeml-792/compiler/parsing]0;Holmake: ~/regression/cakeml-792/compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ~/regression/cakeml-792/characteristic]0;Holmake: ~/regression/cakeml-792/translator]0;Holmake: ~/regression/cakeml-792/translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ~/regression/cakeml-792/characteristic]0;Holmake: ~/regression/cakeml-792/characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: ~/regression/cakeml-792/translator/monadic]0;Holmake: ~/regression/cakeml-792/translator/monadic[1mWorking in $(CAKEMLDIR)/translator/monadic[0m
]0;Holmake: ../reg_alloc/proofs]0;Holmake: ../reg_alloc/proofs[1mWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
]0;Holmake: .]0;Holmake: ../semantics]0;Holmake: ../semantics[1mWorking in $(CAKEMLDIR)/compiler/backend/semantics[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/compiler/backend/proofs[0m
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>
     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.
 
 Exception raised at Tactical.THEN1:
 first subgoal not solved by second tactic (THEN1 on line 1322)
 error in quse /home/myreen/regression/cakeml-792/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"}
 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