Job 1427

CakeML:8881f24e12a03cbd4a514a5f9a96e28183ac811e
  Merge pull request #809 from CakeML/lpr [Jan 03 21:18:47]
HOL:982ebdfbd16f61f3e235ad57dfd4a7bd63936abc
  Prettify sortingScript - use curly quotes and Theorem-syntax more [Jan 04 07:08:13]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Jan 05 10:02:48 Claimed job
Jan 05 10:03:02 Building HOL
Jan 05 10:17:00 Starting developers
Jan 05 10:17:02 Finished developers                                               2s 117MB
Jan 05 10:17:03 Starting developers/bin
Jan 05 10:17:09 Finished developers/bin                                           5s   1GB
Jan 05 10:17:09 Starting semantics/ffi
Jan 05 10:17:19 Finished semantics/ffi                                           10s 318MB
Jan 05 10:17:19 Starting semantics
Jan 05 10:18:51 Finished semantics                                             1m31s   1GB
Jan 05 10:18:51 Starting semantics/proofs
Jan 05 10:22:10 Finished semantics/proofs                                      3m18s   2GB
Jan 05 10:22:10 Starting semantics/alt_semantics
Jan 05 10:22:18 Finished semantics/alt_semantics                                  7s 412MB
Jan 05 10:22:18 Starting semantics/alt_semantics/proofs
Jan 05 10:24:24 Finished semantics/alt_semantics/proofs                        2m06s   1GB
Jan 05 10:24:25 Starting basis/pure
Jan 05 10:27:06 Finished basis/pure                                            2m41s   1GB
Jan 05 10:27:07 Starting translator
Jan 05 10:29:45 Finished translator                                            2m38s   2GB
Jan 05 10:29:45 Starting compiler/parsing
Jan 05 10:30:52 Finished compiler/parsing                                      1m06s   4GB
Jan 05 10:30:52 Starting characteristic
Jan 05 10:36:51 Finished characteristic                                        5m59s   2GB
Jan 05 10:36:52 Starting translator/monadic
Jan 05 10:38:35 Finished translator/monadic                                    1m43s   2GB
Jan 05 10:38:35 Starting basis
Jan 05 11:12:02 Finished basis                                                33m25s  28GB
Jan 05 11:12:02 Starting compiler/inference
Jan 05 11:13:09 Finished compiler/inference                                    1m07s   2GB
Jan 05 11:13:09 Starting compiler/backend/reg_alloc
Jan 05 11:14:13 Finished compiler/backend/reg_alloc                            1m03s   1GB
Jan 05 11:14:13 Starting compiler/backend/gc
Jan 05 11:17:48 Finished compiler/backend/gc                                   3m34s   3GB
Jan 05 11:17:48 Starting compiler/backend
Jan 05 11:22:43 Finished compiler/backend                                      4m55s   4GB
Jan 05 11:22:43 Starting compiler/encoders/asm
Jan 05 11:23:06 Finished compiler/encoders/asm                                   22s   1GB
Jan 05 11:23:06 Starting compiler/encoders/x64
Jan 05 11:24:09 Finished compiler/encoders/x64                                 1m02s   1GB
Jan 05 11:24:09 Starting compiler/encoders/arm7
Jan 05 11:26:11 Finished compiler/encoders/arm7                                2m01s   1GB
Jan 05 11:26:11 Starting compiler/encoders/arm8
Jan 05 11:26:49 Finished compiler/encoders/arm8                                  37s   1GB
Jan 05 11:26:49 Starting compiler/encoders/mips
Jan 05 11:28:14 Finished compiler/encoders/mips                                1m24s   1GB
Jan 05 11:28:14 Starting compiler/encoders/riscv
Jan 05 11:29:51 Finished compiler/encoders/riscv                               1m36s   1GB
Jan 05 11:29:51 Starting compiler/encoders/ag32
Jan 05 11:30:10 Finished compiler/encoders/ag32                                  18s 963MB
Jan 05 11:30:10 Starting compiler/backend/x64
Jan 05 11:30:29 Finished compiler/backend/x64                                    19s   1GB
Jan 05 11:30:29 Starting compiler/backend/arm7
Jan 05 11:30:51 Finished compiler/backend/arm7                                   21s   1GB
Jan 05 11:30:51 Starting compiler/backend/arm8
Jan 05 11:31:11 Finished compiler/backend/arm8                                   20s   1GB
Jan 05 11:31:12 Starting compiler/backend/mips
Jan 05 11:31:32 Finished compiler/backend/mips                                   20s   1GB
Jan 05 11:31:32 Starting compiler/backend/riscv
Jan 05 11:31:54 Finished compiler/backend/riscv                                  22s   1GB
Jan 05 11:31:55 Starting compiler/backend/ag32
Jan 05 11:33:02 Finished compiler/backend/ag32                                 1m06s   2GB
Jan 05 11:33:02 Starting compiler/parsing/proofs
Jan 05 11:38:29 Finished compiler/parsing/proofs                               5m26s   2GB
Jan 05 11:38:29 Starting compiler/inference/proofs
Jan 05 11:41:02 Finished compiler/inference/proofs                             2m32s   2GB
Jan 05 11:41:02 Starting compiler/backend/semantics
Jan 05 12:07:42 Finished compiler/backend/semantics                           26m39s   5GB
Jan 05 12:07:42 Starting compiler/backend/reg_alloc/proofs
Jan 05 12:11:01 Finished compiler/backend/reg_alloc/proofs                     3m18s   1GB
Jan 05 12:11:01 Starting compiler/backend/proofs
Jan 05 12:15:51 FAILED: compiler/backend/proofs
Scanning [1m$(HOLDIR)/examples/machine-code/multiword[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc/lem_lib_stub[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/pattern_matching[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reachability[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/unverified/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/common[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/asm[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/gc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reachability/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/translator[0m
Scanning [1m$(CAKEMLDIR)/characteristic[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/semantics[0m
Starting work on reachable_sptProofTheory
Starting work on README.md
Starting work on bvi_tailrecProofTheory
Starting work on data_liveProofTheory
README.md              real:    0s  user:    0s     OK
Starting work on data_simpProofTheory
...able_sptProofTheory real:   13s  user:   12s     OK
Starting work on data_spaceProofTheory
data_simpProofTheory   real:   16s  user:   16s     OK
Starting work on bvl_constProofTheory
data_spaceProofTheory  real:   30s  user:   28s     OK
Starting work on bvi_letProofTheory
bvi_letProofTheory     real:   22s  user:   20s     OK
Starting work on clos_annotateProofTheory
data_liveProofTheory   real:   74s  user:   72s     OK
Starting work on bvi_to_dataProofTheory
...annotateProofTheory real:   28s  user:   27s     OK
Starting work on clos_callProofTheory
bvl_constProofTheory   real:  107s  user:  103s     OK
Starting work on bvl_handleProofTheory
bvl_handleProofTheory  real:   20s  user:   19s     OK
Starting work on bvl_inlineProofTheory
bvi_tailrecProofTheory real:  181s  user:  178s     OK
Starting work on clos_fvsProofTheory
bvl_inlineProofTheory  real:   35s  user:   33s     OK
Starting work on bvl_to_bviProofTheory
clos_fvsProofTheory    real:   19s  user:   18s     OK
Starting work on clos_knownPropsTheory
clos_knownPropsTheory  real:   13s  user:   12s     OK
Starting work on clos_letopProofTheory
bvi_to_dataProofTheory real:  142s  user:  137s     OK
Starting work on clos_ticksProofTheory
clos_letopProofTheory  real:   21s  user:   20s     OK
Starting work on clos_mtiProofTheory
clos_ticksProofTheory  real:   27s  user:   26s     OK
Starting work on clos_knownProofTheory
clos_mtiProofTheory    real:   39s  user:   37s     OK
Starting work on clos_numberProofTheory
clos_callProofTheory   real:  191s  user:  185s     OK
Starting work on bvl_jumpProofTheory
clos_numberProofTheory real:   11s  user:   10sFAIL<1>
 <<HOL message: Created theory "clos_numberProof">>
 Saved theorem _____ "renumber_code_locs_list_IMP_LENGTH"
 Saved theorem _____ "renumber_code_locs_inc"
 Saved theorem _____ "renumber_code_locs_imp_inc"
 Saved theorem _____ "renumber_code_locs_list_length"
 error in quse /home/myreen/regression/cakeml-1427/compiler/backend/proofs/clos_numberProofScript.sml : HOL_ERR {message = "not an \"==>\"", origin_function = "dest_imp", origin_structure = "boolSyntax"}
 error in load /home/myreen/regression/cakeml-1427/compiler/backend/proofs/clos_numberProofScript : HOL_ERR {message = "not an \"==>\"", origin_function = "dest_imp", origin_structure = "boolSyntax"}
 Uncaught exception: HOL_ERR {message = "not an \"==>\"", origin_function = "dest_imp", origin_structure = "boolSyntax"}
bvl_to_bviProofTheory                          M-KILLED
clos_knownProofTheory                          M-KILLED
bvl_jumpProofTheory                            M-KILLED