Job 1313

CakeML:3f95e30b3a56a7232be14b466ac8bee08db5fbe9
  Fix inferComplete for abbrev changes in HOL master [Aug 04 04:51:11]
HOL:ff3ac4c4c36730c3560764bd9487f22baea5d7a9
  Avoid GC test warnings on low user times, and avoid a MoscowML bug [Jul 29 01:44:39]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Aug 04 09:54:28 Claimed job
Aug 04 09:54:30 Reusing HOL
Aug 04 09:54:36 Starting developers
Aug 04 09:54:39 Finished developers                                               2s 113MB
Aug 04 09:54:39 Starting developers/bin
Aug 04 09:54:45 Finished developers/bin                                           6s   1GB
Aug 04 09:54:45 Starting semantics/ffi
Aug 04 09:54:55 Finished semantics/ffi                                            9s 250MB
Aug 04 09:54:55 Starting semantics
Aug 04 09:56:16 Finished semantics                                             1m20s   1GB
Aug 04 09:56:16 Starting semantics/proofs
Aug 04 09:59:29 Finished semantics/proofs                                      3m13s 996MB
Aug 04 09:59:30 Starting semantics/alt_semantics
Aug 04 09:59:37 Finished semantics/alt_semantics                                  7s 329MB
Aug 04 09:59:37 Starting semantics/alt_semantics/proofs
Aug 04 10:01:43 Finished semantics/alt_semantics/proofs                        2m05s 938MB
Aug 04 10:01:43 Starting basis/pure
Aug 04 10:02:32 Finished basis/pure                                              49s 894MB
Aug 04 10:02:33 Starting translator
Aug 04 10:05:11 Finished translator                                            2m37s   1GB
Aug 04 10:05:11 Starting compiler/parsing
Aug 04 10:06:21 Finished compiler/parsing                                      1m10s   2GB
Aug 04 10:06:21 Starting characteristic
Aug 04 10:13:45 Finished characteristic                                        7m23s   1GB
Aug 04 10:13:45 Starting translator/monadic
Aug 04 10:16:26 Finished translator/monadic                                    2m41s   1GB
Aug 04 10:16:26 Starting basis
Aug 04 10:56:06 Finished basis                                                39m39s  17GB
Aug 04 10:56:06 Starting compiler/inference
Aug 04 10:57:09 Finished compiler/inference                                    1m02s   1GB
Aug 04 10:57:09 Starting compiler/backend/reg_alloc
Aug 04 10:58:16 Finished compiler/backend/reg_alloc                            1m06s   1GB
Aug 04 10:58:16 Starting compiler/backend/gc
Aug 04 11:01:39 Finished compiler/backend/gc                                   3m22s   2GB
Aug 04 11:01:39 Starting compiler/backend
Aug 04 11:06:18 Finished compiler/backend                                      4m38s   4GB
Aug 04 11:06:18 Starting compiler/encoders/asm
Aug 04 11:06:40 Finished compiler/encoders/asm                                   21s 599MB
Aug 04 11:06:40 Starting compiler/encoders/x64
Aug 04 11:07:04 Finished compiler/encoders/x64                                   24s   1GB
Aug 04 11:07:04 Starting compiler/encoders/arm7
Aug 04 11:07:54 Finished compiler/encoders/arm7                                  49s 649MB
Aug 04 11:07:54 Starting compiler/encoders/arm8
Aug 04 11:08:06 Finished compiler/encoders/arm8                                  11s 583MB
Aug 04 11:08:06 Starting compiler/encoders/mips
Aug 04 11:08:23 Finished compiler/encoders/mips                                  16s   1GB
Aug 04 11:08:23 Starting compiler/encoders/riscv
Aug 04 11:08:38 Finished compiler/encoders/riscv                                 14s   1GB
Aug 04 11:08:38 Starting compiler/encoders/ag32
Aug 04 11:08:55 Finished compiler/encoders/ag32                                  16s 889MB
Aug 04 11:08:55 Starting compiler/backend/x64
Aug 04 11:09:12 Finished compiler/backend/x64                                    16s 937MB
Aug 04 11:09:12 Starting compiler/backend/arm7
Aug 04 11:09:32 Finished compiler/backend/arm7                                   19s   1GB
Aug 04 11:09:32 Starting compiler/backend/arm8
Aug 04 11:09:50 Finished compiler/backend/arm8                                   17s   1GB
Aug 04 11:09:50 Starting compiler/backend/mips
Aug 04 11:10:09 Finished compiler/backend/mips                                   19s   1GB
Aug 04 11:10:09 Starting compiler/backend/riscv
Aug 04 11:10:27 Finished compiler/backend/riscv                                  17s 952MB
Aug 04 11:10:27 Starting compiler/backend/ag32
Aug 04 11:11:36 Finished compiler/backend/ag32                                 1m09s   1GB
Aug 04 11:11:36 Starting compiler/parsing/proofs
Aug 04 11:17:18 Finished compiler/parsing/proofs                               5m39s   1GB
Aug 04 11:17:18 Starting compiler/inference/proofs
Aug 04 11:19:44 Finished compiler/inference/proofs                             2m26s   1GB
Aug 04 11:19:45 Starting compiler/backend/semantics
Aug 04 11:50:16 FAILED: compiler/backend/semantics
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
Starting work on README.md
Starting work on backendPropsTheory
Starting work on closSemTheory
Starting work on flatSemTheory
README.md                                                                                                                                            real:    0s  user:    0s     OK
Starting work on wordSemTheory
backendPropsTheory                                                                                                                                   real:   12s  user:   11s     OK
closSemTheory                                                                                                                                        real:   27s  user:   26s     OK
Starting work on bvlSemTheory
Starting work on closPropsTheory
flatSemTheory                                                                                                                                        real:   27s  user:   26s     OK
Starting work on dataSemTheory
bvlSemTheory                                                                                                                                         real:   21s  user:   21s     OK
Starting work on bviSemTheory
wordSemTheory                                                                                                                                        real:   50s  user:   49s     OK
Starting work on flatPropsTheory
bviSemTheory                                                                                                                                         real:   23s  user:   23s     OK
Starting work on targetSemTheory
targetSemTheory                                                                                                                                      real:   19s  user:   19s     OK
Starting work on labSemTheory
labSemTheory                                                                                                                                         real:   27s  user:   26s     OK
Starting work on labPropsTheory
dataSemTheory                                                                                                                                        real:  129s  user:  127s     OK
Starting work on dataPropsTheory
flatPropsTheory                                                                                                                                      real:  106s  user:  104s     OK
Starting work on data_monadTheory
data_monadTheory                                                                                                                                     real:   22s  user:   21s     OK
Starting work on stackSemTheory
labPropsTheory                                                                                                                                       real:   76s  user:   75s     OK
Starting work on targetPropsTheory
targetPropsTheory                                                                                                                                    real:   20s  user:   19s     OK
Starting work on wordPropsTheory
stackSemTheory                                                                                                                                       real:   40s  user:   39s     OK
Starting work on stackPropsTheory
closPropsTheory                                                                                                                                      real:  212s  user:  210s     OK
Starting work on bvlPropsTheory
bvlPropsTheory                                                                                                                                       real:  133s  user:  132s     OK
Starting work on bviPropsTheory
stackPropsTheory                                                                                                                                     real:  170s  user:  168s     OK
bviPropsTheory                                                                                                                                       real:   76s  user:   75s     OK
wordPropsTheory                                                                                                                                      real:  402s  user:  397s     OK
dataPropsTheory                                                                                                                                      real: 1674s  user: 1650sFAIL<1>
     t1. evaluate (prog,t) = (res,t1)  cc_co_only_diff s1 t1
 
 failed.
 Failed to prove theorem evaluate_cc_co_only_diff.
 
 Exception raised at Tactical.THEN1:
 first subgoal not solved by second tactic (THEN1 on line 2623) (THEN1 on line 2660) (THEN1 on line 2663) (THEN1 on line 2668) (THEN1 on line 2672) (THEN1 on line 2676) (THEN1 on line 2683) (THEN1 on line 2695) (THEN1 on line 2706)
 error in quse /home/myreen/regression/cakeml-1313/compiler/backend/semantics/dataPropsScript.sml : HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 2623) (THEN1 on line 2660) (THEN1 on line 2663) (THEN1 on line 2668) (THEN1 on line 2672) (THEN1 on line 2676) (THEN1 on line 2683) (THEN1 on line 2695) (THEN1 on line 2706)", origin_function = "THEN1", origin_structure = "Tactical"}
 error in load /home/myreen/regression/cakeml-1313/compiler/backend/semantics/dataPropsScript : HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 2623) (THEN1 on line 2660) (THEN1 on line 2663) (THEN1 on line 2668) (THEN1 on line 2672) (THEN1 on line 2676) (THEN1 on line 2683) (THEN1 on line 2695) (THEN1 on line 2706)", origin_function = "THEN1", origin_structure = "Tactical"}
 Uncaught exception: HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 2623) (THEN1 on line 2660) (THEN1 on line 2663) (THEN1 on line 2668) (THEN1 on line 2672) (THEN1 on line 2676) (THEN1 on line 2683) (THEN1 on line 2695) (THEN1 on line 2706)", origin_function = "THEN1", origin_structure = "Tactical"}