Job 1142

CakeML:8d0a27d80019b814d040fabcd997768d263a267c
  Break a very long line [Jan 08 00:38:31]
#715 (unsafe-accesses)
Merging into:6f499a68f2500e7f937b3254c9da6f93a9b62670
  Merge pull request #716 from CakeML/stack-opt-2 [Jan 09 03:33:21]
HOL:1f867f177143c9ba9b92ec32d874c1f2514b5322
  Optimise DefnBase.one_line_ify slightly in presence of many literals [Jan 11 05:29:17]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Jan 12 19:54:08 Claimed job
Jan 12 19:54:16 Building HOL
Jan 12 20:03:52 Starting developers
Jan 12 20:03:53 Finished developers                                               0s  21MB
Jan 12 20:03:53 Starting developers/bin
Jan 12 20:03:57 Finished developers/bin                                           3s 240MB
Jan 12 20:03:57 Starting semantics/ffi
Jan 12 20:04:05 Finished semantics/ffi                                            7s 247MB
Jan 12 20:04:05 Starting semantics
Jan 12 20:05:30 Finished semantics                                             1m24s   1GB
Jan 12 20:05:31 Starting semantics/proofs
Jan 12 20:08:44 Finished semantics/proofs                                      3m13s   1GB
Jan 12 20:08:44 Starting semantics/alt_semantics
Jan 12 20:08:51 Finished semantics/alt_semantics                                  6s 279MB
Jan 12 20:08:51 Starting semantics/alt_semantics/proofs
Jan 12 20:10:51 Finished semantics/alt_semantics/proofs                        1m59s 796MB
Jan 12 20:10:52 Starting basis/pure
Jan 12 20:13:47 Finished basis/pure                                            2m55s 848MB
Jan 12 20:13:48 Starting translator
Jan 12 20:16:20 Finished translator                                            2m32s   1GB
Jan 12 20:16:20 Starting compiler/parsing
Jan 12 20:17:26 Finished compiler/parsing                                      1m05s   2GB
Jan 12 20:17:26 Starting characteristic
Jan 12 20:22:56 Finished characteristic                                        5m29s   2GB
Jan 12 20:22:56 Starting translator/monadic
Jan 12 20:24:24 Finished translator/monadic                                    1m27s   1GB
Jan 12 20:24:25 Starting basis
Jan 12 20:57:45 Finished basis                                                33m19s  18GB
Jan 12 20:57:45 Starting compiler/inference
Jan 12 20:59:53 Finished compiler/inference                                    2m07s   3GB
Jan 12 20:59:53 Starting compiler/backend/reg_alloc
Jan 12 21:00:53 Finished compiler/backend/reg_alloc                              59s   1GB
Jan 12 21:00:53 Starting compiler/backend/gc
Jan 12 21:04:06 Finished compiler/backend/gc                                   3m12s   2GB
Jan 12 21:04:07 Starting compiler/backend
Jan 12 21:08:27 Finished compiler/backend                                      4m20s   2GB
Jan 12 21:08:28 Starting compiler/encoders/asm
Jan 12 21:08:48 Finished compiler/encoders/asm                                   20s 524MB
Jan 12 21:08:48 Starting compiler/encoders/x64
Jan 12 21:09:40 Finished compiler/encoders/x64                                   50s 965MB
Jan 12 21:09:40 Starting compiler/encoders/arm7
Jan 12 21:11:18 Finished compiler/encoders/arm7                                1m37s   1GB
Jan 12 21:11:18 Starting compiler/encoders/arm8
Jan 12 21:11:48 Finished compiler/encoders/arm8                                  29s 549MB
Jan 12 21:11:48 Starting compiler/encoders/mips
Jan 12 21:12:54 Finished compiler/encoders/mips                                1m06s   1GB
Jan 12 21:12:55 Starting compiler/encoders/riscv
Jan 12 21:14:16 Finished compiler/encoders/riscv                               1m20s   1GB
Jan 12 21:14:16 Starting compiler/encoders/ag32
Jan 12 21:14:32 Finished compiler/encoders/ag32                                  15s 504MB
Jan 12 21:14:32 Starting compiler/backend/x64
Jan 12 21:14:49 Finished compiler/backend/x64                                    16s   1GB
Jan 12 21:14:49 Starting compiler/backend/arm7
Jan 12 21:15:08 Finished compiler/backend/arm7                                   19s   1GB
Jan 12 21:15:09 Starting compiler/backend/arm8
Jan 12 21:15:27 Finished compiler/backend/arm8                                   17s   1GB
Jan 12 21:15:27 Starting compiler/backend/mips
Jan 12 21:15:45 Finished compiler/backend/mips                                   17s   1GB
Jan 12 21:15:45 Starting compiler/backend/riscv
Jan 12 21:16:02 Finished compiler/backend/riscv                                  16s   1GB
Jan 12 21:16:02 Starting compiler/backend/ag32
Jan 12 21:17:08 Finished compiler/backend/ag32                                 1m05s   1GB
Jan 12 21:17:08 Starting compiler/parsing/proofs
Jan 12 21:22:29 Finished compiler/parsing/proofs                               5m20s 909MB
Jan 12 21:22:29 Starting compiler/inference/proofs
Jan 12 21:25:20 Finished compiler/inference/proofs                             2m50s   1GB
Jan 12 21:25:20 Starting compiler/backend/semantics
Jan 12 21:51:50 Finished compiler/backend/semantics                           26m29s   2GB
Jan 12 21:51:50 Starting compiler/backend/reg_alloc/proofs
Jan 12 21:55:07 Finished compiler/backend/reg_alloc/proofs                     3m16s 764MB
Jan 12 21:55:08 Starting compiler/backend/proofs
Jan 12 22:54:47 Finished compiler/backend/proofs                              59m38s  19GB
Jan 12 22:54:47 Starting compiler/encoders/x64/proofs
Jan 12 23:03:54 Finished compiler/encoders/x64/proofs                          9m06s   5GB
Jan 12 23:03:54 Starting compiler/encoders/arm7/proofs
Jan 12 23:16:13 Finished compiler/encoders/arm7/proofs                        12m19s   3GB
Jan 12 23:16:14 Starting compiler/encoders/arm8/proofs
Jan 12 23:22:28 Finished compiler/encoders/arm8/proofs                         6m13s   1GB
Jan 12 23:22:28 Starting compiler/encoders/mips/proofs
Jan 12 23:31:47 Finished compiler/encoders/mips/proofs                         9m18s   3GB
Jan 12 23:31:47 Starting compiler/encoders/riscv/proofs
Jan 12 23:40:11 Finished compiler/encoders/riscv/proofs                        8m23s   1GB
Jan 12 23:40:11 Starting compiler/encoders/ag32/proofs
Jan 12 23:42:34 Finished compiler/encoders/ag32/proofs                         2m22s   1GB
Jan 12 23:42:35 Starting compiler/backend/x64/proofs
Jan 12 23:42:52 Finished compiler/backend/x64/proofs                             17s   1GB
Jan 12 23:42:52 Starting compiler/backend/arm7/proofs
Jan 12 23:43:10 Finished compiler/backend/arm7/proofs                            17s   1GB
Jan 12 23:43:11 Starting compiler/backend/arm8/proofs
Jan 12 23:43:28 Finished compiler/backend/arm8/proofs                            16s   1GB
Jan 12 23:43:28 Starting compiler/backend/mips/proofs
Jan 12 23:43:46 Finished compiler/backend/mips/proofs                            17s   1GB
Jan 12 23:43:46 Starting compiler/backend/riscv/proofs
Jan 12 23:44:04 Finished compiler/backend/riscv/proofs                           17s   1GB
Jan 12 23:44:04 Starting compiler/backend/ag32/proofs
Jan 12 23:53:09 Finished compiler/backend/ag32/proofs                          9m04s   2GB
Jan 12 23:53:09 Starting compiler/proofs
Jan 12 23:54:41 Finished compiler/proofs                                       1m31s   3GB
Jan 12 23:54:41 Starting candle/set-theory
Jan 12 23:55:08 Finished candle/set-theory                                       26s 859MB
Jan 12 23:55:09 Starting candle/syntax-lib
Jan 12 23:55:18 Finished candle/syntax-lib                                        9s 625MB
Jan 12 23:55:19 Starting candle/standard/syntax
Jan 12 23:57:02 Finished candle/standard/syntax                                1m42s 843MB
Jan 12 23:57:02 Starting candle/standard/semantics
Jan 12 23:58:38 Finished candle/standard/semantics                             1m35s   1GB
Jan 12 23:58:38 Starting candle/standard/monadic
Jan 13 00:00:13 Finished candle/standard/monadic                               1m34s   1GB
Jan 13 00:00:14 Starting candle/standard/ml_kernel
Jan 13 00:05:18 Finished candle/standard/ml_kernel                             5m04s   3GB
Jan 13 00:05:18 Starting candle/standard/opentheory
Jan 13 00:14:13 Finished candle/standard/opentheory                            8m54s   4GB
Jan 13 00:14:13 Starting candle/standard/opentheory/compilation
Jan 13 00:46:44 Finished candle/standard/opentheory/compilation               32m30s  16GB
Jan 13 00:46:45 Starting candle/standard/opentheory/compilation/proofs
Jan 13 00:47:22 Finished candle/standard/opentheory/compilation/proofs           36s   3GB
Jan 13 00:47:22 Starting characteristic/examples
Jan 13 00:48:51 Finished characteristic/examples                               1m27s   2GB
Jan 13 00:48:51 Starting tutorial/solutions
Jan 13 01:02:52 Finished tutorial/solutions                                   14m00s   6GB
Jan 13 01:02:52 Starting translator/monadic/examples
Jan 13 01:05:49 Finished translator/monadic/examples                           2m56s   2GB
Jan 13 01:05:49 Starting examples
Jan 13 01:15:13 Finished examples                                              9m23s   3GB
Jan 13 01:15:13 Starting examples/compilation/x64
Jan 13 03:28:14 Finished examples/compilation/x64                           2h13m00s  12GB
Jan 13 03:28:14 Starting examples/compilation/x64/proofs
Jan 13 03:30:27 Finished examples/compilation/x64/proofs                       2m12s   2GB
Jan 13 03:30:27 Starting examples/compilation/ag32
Jan 13 04:00:37 Finished examples/compilation/ag32                            30m09s   6GB
Jan 13 04:00:38 Starting examples/compilation/ag32/proofs
Jan 13 04:01:29 Finished examples/compilation/ag32/proofs                        50s   3GB
Jan 13 04:01:29 Starting examples/cost
Jan 13 04:29:08 Finished examples/cost                                        27m37s  11GB
Jan 13 04:29:09 Starting examples/lrat_checker
Jan 13 04:32:32 Finished examples/lrat_checker                                 3m22s   2GB
Jan 13 04:32:32 Starting examples/lrat_checker/compilation
Jan 13 04:49:17 Finished examples/lrat_checker/compilation                    16m44s   8GB
Jan 13 04:49:17 Starting examples/lrat_checker/compilation/proofs
Jan 13 04:50:04 Finished examples/lrat_checker/compilation/proofs                46s   2GB
Jan 13 04:50:04 Starting examples/lrat_checker/array
Jan 13 04:56:21 Finished examples/lrat_checker/array                           6m16s   3GB
Jan 13 04:56:21 Starting examples/lrat_checker/array/compilation
Jan 13 05:10:53 Finished examples/lrat_checker/array/compilation              14m31s  10GB
Jan 13 05:10:53 Starting examples/lrat_checker/array/compilation/proofs
Jan 13 05:11:40 Finished examples/lrat_checker/array/compilation/proofs          46s   2GB
Jan 13 05:11:40 Starting translator/okasaki-examples
Jan 13 05:15:53 Finished translator/okasaki-examples                           4m12s   1GB
Jan 13 05:15:54 Starting translator/other-examples
Jan 13 05:17:39 Finished translator/other-examples                             1m45s   1GB
Jan 13 05:17:39 Starting compiler/parsing/tests
Jan 13 05:18:04 Finished compiler/parsing/tests                                  24s 600MB
Jan 13 05:18:04 Starting compiler/inference/tests
Jan 13 05:22:31 Finished compiler/inference/tests                              4m26s   3GB
Jan 13 05:22:31 Starting compiler/bootstrap/translation
Jan 13 08:44:23 FAILED: compiler/bootstrap/translation
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/common[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/lib[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/model[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
Scanning [1m$(HOLDIR)/examples/formal-languages[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/parsing[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/translator[0m
Scanning [1m$(CAKEMLDIR)/characteristic[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic[0m
Scanning [1m$(CAKEMLDIR)/basis[0m
Scanning [1m$(HOLDIR)/examples/machine-code/multiword[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reachability[0m
Scanning [1m$(CAKEMLDIR)/unverified/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/asm[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/ag32[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/ag32[0m
Scanning [1m$(HOLDIR)/examples/machine-code/decompiler[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm7[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm7[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm8[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm8[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/mips[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/mips[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/riscv[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/riscv[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/x64[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/x64[0m
Scanning [1m$(HOLDIR)/examples/unification/triangular[0m
Scanning [1m$(HOLDIR)/examples/unification/triangular/first-order[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference[0m
Scanning [1m$(CAKEMLDIR)/compiler[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/monadic_enc[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference/proofs[0m
Starting work on monadic_encTheory
Starting work on to_flatProgTheory
monadic_encTheory                                                             real:    9s  user:    8s     OK
Starting work on monadic_enc32Theory
Starting work on monadic_enc64Theory
monadic_enc64Theory                                                           real:   13s  user:   12s     OK
monadic_enc32Theory                                                           real:   13s  user:   13s     OK
to_flatProgTheory                                                             real:  345s  user:  341s     OK
Starting work on to_patProgTheory
to_patProgTheory                                                              real:  106s  user:  104s     OK
Starting work on to_closProgTheory
to_closProgTheory                                                             real:  452s  user:  446s     OK
Starting work on to_bvlProgTheory
to_bvlProgTheory                                                              real:  348s  user:  344s     OK
Starting work on to_bviProgTheory
to_bviProgTheory                                                              real:  305s  user:  301s     OK
Starting work on to_dataProgTheory
to_dataProgTheory                                                             real:  161s  user:  159s     OK
Starting work on lexerProgTheory
lexerProgTheory                                                               real:  248s  user:  245s     OK
Starting work on parserProgTheory
parserProgTheory                                                              real:  485s  user:  476s     OK
Starting work on reg_allocProgTheory
reg_allocProgTheory                                                           real:  840s  user:  831s     OK
Starting work on inferProgTheory
inferProgTheory                                                               real: 4617s  user: 4565s     OK
Starting work on explorerProgTheory
explorerProgTheory                                                            real: 1059s  user: 1053s     OK
Starting work on sexp_parserProgTheory
sexp_parserProgTheory                                                         real:  262s  user:  256s     OK
Starting work on to_word32ProgTheory
Starting work on to_word64ProgTheory
to_word64ProgTheory                                                           real:  999s  user:  984s     OK
Starting work on to_target64ProgTheory
to_word32ProgTheory                                                           real: 1012s  user:  993s     OK
Starting work on to_target32ProgTheory
to_target64ProgTheory                                                         real:  633s  user:  613s     OK
Starting work on x64ProgTheory
to_target32ProgTheory                                                         real:  640s  user:  619s     OK
Starting work on arm7ProgTheory
x64ProgTheory                                                                 real:  234s  user:  228s     OK
Starting work on arm8ProgTheory
arm7ProgTheory                                                                real:  268s  user:  264s     OK
Starting work on ag32ProgTheory
arm8ProgTheory                                                                real:  239s  user:  234s     OK
Starting work on riscvProgTheory
ag32ProgTheory                                                                real:  202s  user:  195s     OK
Starting work on compiler32ProgTheory
riscvProgTheory                                                               real:  253s  user:  249s     OK
Starting work on mipsProgTheory
mipsProgTheory                                                                real:  214s  user:  210s     OK
Starting work on compiler64ProgTheory
compiler32ProgTheory                                                          real:  748s  user:  726sFAIL<1>
        COMMANDLINE cl)
 
 failed.
 Failed to prove theorem main_spec.
 
 Exception raised at Tactical.THEN1:
 first subgoal not solved by second tactic (THEN1 on line 293) (THEN1 on line 298) (THEN1 on line 302)
 error in quse /home/myreen/regression/cakeml-1142/compiler/bootstrap/translation/compiler32ProgScript.sml : HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 293) (THEN1 on line 298) (THEN1 on line 302)", origin_function = "THEN1", origin_structure = "Tactical"}
 error in load /home/myreen/regression/cakeml-1142/compiler/bootstrap/translation/compiler32ProgScript : HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 293) (THEN1 on line 298) (THEN1 on line 302)", origin_function = "THEN1", origin_structure = "Tactical"}
 Uncaught exception: HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 293) (THEN1 on line 298) (THEN1 on line 302)", origin_function = "THEN1", origin_structure = "Tactical"}
compiler64ProgTheory                                                                                  M-KILLED