Job 1102

CakeML:7b87910df6cbded9e042bdb65e8ff0352cb7c754
  Merge remote-tracking branch 'origin/data-cost-gen' into data-cost [Nov 26 20:54:49]
#707 (data-cost)
Merging into:6d749b2319ab6ff64a20cb67bc860ce939255992
  Fix two scripts broken by removal of big-record optimisation [Nov 25 04:15:27]
HOL:ad87bf11e5978fea7829defa6bb7ead073b71380
  Slightly recast core result about  [Nov 23 11:06:58]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Nov 26 20:57:19 Claimed job
Nov 26 20:57:26 Building HOL
Nov 26 21:10:52 Starting developers
Nov 26 21:10:55 Finished developers                                               2s 127MB
Nov 26 21:10:55 Starting developers/bin
Nov 26 21:11:00 Finished developers/bin                                           3s 238MB
Nov 26 21:11:00 Starting semantics/ffi
Nov 26 21:11:11 Finished semantics/ffi                                           10s 221MB
Nov 26 21:11:11 Starting semantics
Nov 26 21:13:23 Finished semantics                                             2m11s   1GB
Nov 26 21:13:23 Starting semantics/proofs
Nov 26 21:18:07 Finished semantics/proofs                                      4m43s 997MB
Nov 26 21:18:07 Starting semantics/alt_semantics
Nov 26 21:18:16 Finished semantics/alt_semantics                                  8s 304MB
Nov 26 21:18:16 Starting semantics/alt_semantics/proofs
Nov 26 21:21:02 Finished semantics/alt_semantics/proofs                        2m45s 855MB
Nov 26 21:21:02 Starting basis/pure
Nov 26 21:25:24 Finished basis/pure                                            4m20s 885MB
Nov 26 21:25:24 Starting translator
Nov 26 21:28:19 Finished translator                                            2m54s   1GB
Nov 26 21:28:19 Starting compiler/parsing
Nov 26 21:30:19 Finished compiler/parsing                                      1m59s   1GB
Nov 26 21:30:19 Starting characteristic
Nov 26 21:37:39 Finished characteristic                                        7m18s   2GB
Nov 26 21:37:39 Starting translator/monadic
Nov 26 21:39:45 Finished translator/monadic                                    2m06s   1GB
Nov 26 21:39:46 Starting basis
Nov 26 22:07:38 Finished basis                                                27m52s   3GB
Nov 26 22:07:38 Starting compiler/inference
Nov 26 22:09:32 Finished compiler/inference                                    1m53s   1GB
Nov 26 22:09:32 Starting compiler/backend/reg_alloc
Nov 26 22:10:40 Finished compiler/backend/reg_alloc                            1m08s   1GB
Nov 26 22:10:41 Starting compiler/backend/gc
Nov 26 22:14:39 Finished compiler/backend/gc                                   3m58s   1GB
Nov 26 22:14:39 Starting compiler/backend
Nov 26 22:19:29 Finished compiler/backend                                      4m49s   2GB
Nov 26 22:19:30 Starting compiler/encoders/asm
Nov 26 22:19:51 Finished compiler/encoders/asm                                   21s 804MB
Nov 26 22:19:52 Starting compiler/encoders/x64
Nov 26 22:20:50 Finished compiler/encoders/x64                                   58s 966MB
Nov 26 22:20:50 Starting compiler/encoders/arm7
Nov 26 22:22:38 Finished compiler/encoders/arm7                                1m47s   1GB
Nov 26 22:22:38 Starting compiler/encoders/arm8
Nov 26 22:23:13 Finished compiler/encoders/arm8                                  33s 576MB
Nov 26 22:23:13 Starting compiler/encoders/mips
Nov 26 22:24:27 Finished compiler/encoders/mips                                1m13s   1GB
Nov 26 22:24:27 Starting compiler/encoders/riscv
Nov 26 22:25:53 Finished compiler/encoders/riscv                               1m25s 984MB
Nov 26 22:25:53 Starting compiler/encoders/ag32
Nov 26 22:26:11 Finished compiler/encoders/ag32                                  17s 569MB
Nov 26 22:26:11 Starting compiler/backend/x64
Nov 26 22:26:30 Finished compiler/backend/x64                                    18s   1GB
Nov 26 22:26:30 Starting compiler/backend/arm7
Nov 26 22:26:51 Finished compiler/backend/arm7                                   20s   1GB
Nov 26 22:26:51 Starting compiler/backend/arm8
Nov 26 22:27:10 Finished compiler/backend/arm8                                   18s   1GB
Nov 26 22:27:11 Starting compiler/backend/mips
Nov 26 22:27:30 Finished compiler/backend/mips                                   18s   1GB
Nov 26 22:27:30 Starting compiler/backend/riscv
Nov 26 22:27:49 Finished compiler/backend/riscv                                  18s   1GB
Nov 26 22:27:49 Starting compiler/backend/ag32
Nov 26 22:29:02 Finished compiler/backend/ag32                                 1m12s   1GB
Nov 26 22:29:02 Starting compiler/parsing/proofs
Nov 26 22:34:45 Finished compiler/parsing/proofs                               5m42s 885MB
Nov 26 22:34:45 Starting compiler/inference/proofs
Nov 26 22:37:36 Finished compiler/inference/proofs                             2m51s   1GB
Nov 26 22:37:36 Starting compiler/backend/semantics
Nov 26 22:57:08 Finished compiler/backend/semantics                           19m31s   2GB
Nov 26 22:57:08 Starting compiler/backend/reg_alloc/proofs
Nov 26 23:00:27 Finished compiler/backend/reg_alloc/proofs                     3m18s   1GB
Nov 26 23:00:27 Starting compiler/backend/proofs
Nov 26 23:57:05 Finished compiler/backend/proofs                              56m37s  17GB
Nov 26 23:57:06 Starting compiler/encoders/x64/proofs
Nov 27 00:06:14 Finished compiler/encoders/x64/proofs                          9m08s   5GB
Nov 27 00:06:14 Starting compiler/encoders/arm7/proofs
Nov 27 00:18:41 Finished compiler/encoders/arm7/proofs                        12m26s   3GB
Nov 27 00:18:42 Starting compiler/encoders/arm8/proofs
Nov 27 00:24:59 Finished compiler/encoders/arm8/proofs                         6m16s   1GB
Nov 27 00:24:59 Starting compiler/encoders/mips/proofs
Nov 27 00:34:12 Finished compiler/encoders/mips/proofs                         9m13s   2GB
Nov 27 00:34:13 Starting compiler/encoders/riscv/proofs
Nov 27 00:42:43 Finished compiler/encoders/riscv/proofs                        8m30s   1GB
Nov 27 00:42:44 Starting compiler/encoders/ag32/proofs
Nov 27 00:45:09 Finished compiler/encoders/ag32/proofs                         2m25s 836MB
Nov 27 00:45:09 Starting compiler/backend/x64/proofs
Nov 27 00:45:27 Finished compiler/backend/x64/proofs                             17s   1GB
Nov 27 00:45:27 Starting compiler/backend/arm7/proofs
Nov 27 00:45:45 Finished compiler/backend/arm7/proofs                            17s 971MB
Nov 27 00:45:45 Starting compiler/backend/arm8/proofs
Nov 27 00:46:03 Finished compiler/backend/arm8/proofs                            17s   1GB
Nov 27 00:46:03 Starting compiler/backend/mips/proofs
Nov 27 00:46:21 Finished compiler/backend/mips/proofs                            17s   1GB
Nov 27 00:46:21 Starting compiler/backend/riscv/proofs
Nov 27 00:46:39 Finished compiler/backend/riscv/proofs                           17s   1GB
Nov 27 00:46:39 Starting compiler/backend/ag32/proofs
Nov 27 00:55:44 Finished compiler/backend/ag32/proofs                          9m04s   2GB
Nov 27 00:55:44 Starting compiler/proofs
Nov 27 00:57:17 Finished compiler/proofs                                       1m32s   4GB
Nov 27 00:57:17 Starting candle/set-theory
Nov 27 00:57:44 Finished candle/set-theory                                       26s 757MB
Nov 27 00:57:45 Starting candle/syntax-lib
Nov 27 00:57:54 Finished candle/syntax-lib                                        9s 563MB
Nov 27 00:57:54 Starting candle/standard/syntax
Nov 27 00:59:38 Finished candle/standard/syntax                                1m43s   1GB
Nov 27 00:59:39 Starting candle/standard/semantics
Nov 27 01:01:14 Finished candle/standard/semantics                             1m35s   1GB
Nov 27 01:01:14 Starting candle/standard/monadic
Nov 27 01:02:48 Finished candle/standard/monadic                               1m33s   1GB
Nov 27 01:02:48 Starting candle/standard/ml_kernel
Nov 27 01:06:42 Finished candle/standard/ml_kernel                             3m53s   3GB
Nov 27 01:06:42 Starting candle/standard/opentheory
Nov 27 01:15:22 Finished candle/standard/opentheory                            8m39s   4GB
Nov 27 01:15:22 Starting candle/standard/opentheory/compilation
Nov 27 01:45:22 Finished candle/standard/opentheory/compilation               29m59s  17GB
Nov 27 01:45:22 Starting candle/standard/opentheory/compilation/proofs
Nov 27 01:46:08 Finished candle/standard/opentheory/compilation/proofs           44s   2GB
Nov 27 01:46:08 Starting characteristic/examples
Nov 27 01:47:38 Finished characteristic/examples                               1m29s   2GB
Nov 27 01:47:38 Starting tutorial/solutions
Nov 27 02:01:15 Finished tutorial/solutions                                   13m36s   7GB
Nov 27 02:01:15 Starting translator/monadic/examples
Nov 27 02:04:07 Finished translator/monadic/examples                           2m51s   2GB
Nov 27 02:04:07 Starting examples
Nov 27 02:13:12 Finished examples                                              9m05s   4GB
Nov 27 02:13:13 Starting examples/compilation/x64
Nov 27 04:17:34 Finished examples/compilation/x64                           2h04m20s  14GB
Nov 27 04:17:34 Starting examples/compilation/x64/proofs
Nov 27 04:19:17 Finished examples/compilation/x64/proofs                       1m42s   2GB
Nov 27 04:19:17 Starting examples/compilation/ag32
Nov 27 04:48:24 Finished examples/compilation/ag32                            29m06s   6GB
Nov 27 04:48:24 Starting examples/compilation/ag32/proofs
Nov 27 04:49:04 Finished examples/compilation/ag32/proofs                        39s   2GB
Nov 27 04:49:05 Starting examples/cost
Nov 27 05:10:54 Finished examples/cost                                        21m49s   6GB
Nov 27 05:10:54 Starting translator/okasaki-examples
Nov 27 05:15:06 Finished translator/okasaki-examples                           4m11s   1GB
Nov 27 05:15:07 Starting translator/other-examples
Nov 27 05:16:49 Finished translator/other-examples                             1m42s   1GB
Nov 27 05:16:50 Starting compiler/parsing/tests
Nov 27 05:17:13 Finished compiler/parsing/tests                                  23s 462MB
Nov 27 05:17:13 Starting compiler/inference/tests
Nov 27 05:21:34 Finished compiler/inference/tests                              4m20s   3GB
Nov 27 05:21:34 Starting compiler/bootstrap/translation
Nov 27 07:38:42 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 README.md
Starting work on to_flatProgTheory
README.md                                                                     real:    0s  user:    0s     OK
monadic_encTheory                                                             real:    9s  user:    9s     OK
Starting work on monadic_enc32Theory
Starting work on monadic_enc64Theory
monadic_enc64Theory                                                           real:   13s  user:   13s     OK
monadic_enc32Theory                                                           real:   13s  user:   13s     OK
to_flatProgTheory                                                             real:  313s  user:  309s     OK
Starting work on to_patProgTheory
to_patProgTheory                                                              real:   99s  user:   97s     OK
Starting work on to_closProgTheory
to_closProgTheory                                                             real:  441s  user:  436s     OK
Starting work on to_bvlProgTheory
to_bvlProgTheory                                                              real:  229s  user:  224s     OK
Starting work on to_bviProgTheory
to_bviProgTheory                                                              real:  301s  user:  296s     OK
Starting work on to_dataProgTheory
to_dataProgTheory                                                             real:  172s  user:  170s     OK
Starting work on lexerProgTheory
lexerProgTheory                                                               real:  248s  user:  245s     OK
Starting work on parserProgTheory
parserProgTheory                                                              real:  477s  user:  469s     OK
Starting work on reg_allocProgTheory
reg_allocProgTheory                                                           real:  831s  user:  823s     OK
Starting work on inferProgTheory
inferProgTheory                                                               real: 1150s  user: 1138s     OK
Starting work on explorerProgTheory
explorerProgTheory                                                            real: 1051s  user: 1047s     OK
Starting work on sexp_parserProgTheory
sexp_parserProgTheory                                                         real:  257s  user:  251s     OK
Starting work on to_word32ProgTheory
Starting work on to_word64ProgTheory
to_word64ProgTheory                                                           real:  942s  user:  923s     OK
Starting work on to_target64ProgTheory
to_word32ProgTheory                                                           real:  944s  user:  925s     OK
Starting work on to_target32ProgTheory
to_target64ProgTheory                                                         real:  570s  user:  552s     OK
Starting work on x64ProgTheory
to_target32ProgTheory                                                         real:  613s  user:  578s     OK
Starting work on arm7ProgTheory
arm7ProgTheory                                                                real:  269s  user:  266s     OK
Starting work on ag32ProgTheory
x64ProgTheory                                                                 real:  315s  user:  307s     OK
Starting work on arm8ProgTheory
ag32ProgTheory                                                                real:  178s  user:  174s     OK
Starting work on compiler32ProgTheory
arm8ProgTheory                                                                real:  244s  user:  239s     OK
Starting work on riscvProgTheory
riscvProgTheory                                                               real:  249s  user:  245s     OK
Starting work on mipsProgTheory
mipsProgTheory                                                                real:  210s  user:  206s     OK
Starting work on compiler64ProgTheory
compiler32ProgTheory                                                          real:  640s  user:  619sFAIL<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-1102/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-1102/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