Job 689

CakeML:4c7bf47ab5ec3da9da1e0f994b560d0342f6e9e1
  Merge pull request #604 from Gaj7/master [Jan 16 14:54:23]
HOL:ce7414f3a9b67a55c010a5194ca0029e347b7810
  More easily moved theorems from CakeML (this time to finite_map) [Jan 17 00:42:39]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Jan 18 04:04:12 Claimed job
Jan 18 04:04:21 Building HOL
Jan 18 04:12:01 Starting developers
Jan 18 04:12:02 Finished developers                                               0s  38MB
Jan 18 04:12:03 Starting developers/bin
Jan 18 04:12:33 Finished developers/bin                                          29s 140MB
Jan 18 04:12:34 Starting semantics/ffi
Jan 18 04:13:08 Finished semantics/ffi                                           33s 344MB
Jan 18 04:13:09 Starting semantics
Jan 18 04:14:42 Finished semantics                                             1m32s   1GB
Jan 18 04:14:43 Starting semantics/proofs
Jan 18 04:17:58 Finished semantics/proofs                                      3m14s   1GB
Jan 18 04:17:59 Starting basis/pure
Jan 18 04:21:34 Finished basis/pure                                            3m34s 680MB
Jan 18 04:21:34 Starting translator
Jan 18 04:23:15 Finished translator                                            1m39s   1GB
Jan 18 04:23:16 Starting compiler/parsing
Jan 18 04:24:20 Finished compiler/parsing                                      1m03s   1GB
Jan 18 04:24:21 Starting characteristic
Jan 18 04:27:35 Finished characteristic                                        3m13s   1GB
Jan 18 04:27:36 Starting translator/monadic
Jan 18 04:29:00 Finished translator/monadic                                    1m23s   1GB
Jan 18 04:29:01 Starting basis
Jan 18 04:44:46 Finished basis                                                15m44s   2GB
Jan 18 04:44:47 Starting compiler/inference
Jan 18 04:46:41 Finished compiler/inference                                    1m53s   1GB
Jan 18 04:46:42 Starting compiler/backend/reg_alloc
Jan 18 04:47:33 Finished compiler/backend/reg_alloc                              50s   1GB
Jan 18 04:47:34 Starting compiler/backend/gc
Jan 18 04:56:24 Finished compiler/backend/gc                                   8m48s   1GB
Jan 18 04:56:24 Starting compiler/backend
Jan 18 04:56:27 Finished compiler/backend                                         1s  30MB
Jan 18 04:56:27 Starting compiler/encoders/asm
Jan 18 04:56:29 Finished compiler/encoders/asm                                    0s  17MB
Jan 18 04:56:30 Starting compiler/encoders/x64
Jan 18 04:57:29 Finished compiler/encoders/x64                                   58s 609MB
Jan 18 04:57:30 Starting compiler/encoders/arm6
Jan 18 04:59:17 Finished compiler/encoders/arm6                                1m46s   1GB
Jan 18 04:59:18 Starting compiler/encoders/arm8
Jan 18 04:59:48 Finished compiler/encoders/arm8                                  29s 796MB
Jan 18 04:59:49 Starting compiler/encoders/mips
Jan 18 05:00:53 Finished compiler/encoders/mips                                1m02s   1GB
Jan 18 05:00:54 Starting compiler/encoders/riscv
Jan 18 05:02:02 Finished compiler/encoders/riscv                               1m06s 972MB
Jan 18 05:02:02 Starting compiler/encoders/ag32
Jan 18 05:02:19 Finished compiler/encoders/ag32                                  15s 775MB
Jan 18 05:02:20 Starting compiler/backend/x64
Jan 18 05:02:36 Finished compiler/backend/x64                                    15s 796MB
Jan 18 05:02:37 Starting compiler/backend/arm6
Jan 18 05:02:56 Finished compiler/backend/arm6                                   18s   1GB
Jan 18 05:02:57 Starting compiler/backend/arm8
Jan 18 05:03:15 Finished compiler/backend/arm8                                   16s   1GB
Jan 18 05:03:15 Starting compiler/backend/mips
Jan 18 05:03:33 Finished compiler/backend/mips                                   17s   1GB
Jan 18 05:03:34 Starting compiler/backend/riscv
Jan 18 05:03:52 Finished compiler/backend/riscv                                  16s   1GB
Jan 18 05:03:52 Starting compiler/backend/ag32
Jan 18 05:05:05 Finished compiler/backend/ag32                                 1m12s   1GB
Jan 18 05:05:06 Starting compiler/parsing/proofs
Jan 18 05:10:57 Finished compiler/parsing/proofs                               5m50s 972MB
Jan 18 05:10:58 Starting compiler/inference/proofs
Jan 18 05:13:51 Finished compiler/inference/proofs                             2m52s 996MB
Jan 18 05:13:52 Starting compiler/backend/semantics
Jan 18 05:19:10 FAILED: compiler/backend/semantics
]0;Holmake: ~/regression/HOL-ce7414f3a9b67a55c010a5194ca0029e347b7810/examples/machine-code/multiword]0;Holmake: ~/regression/HOL-ce7414f3a9b67a55c010a5194ca0029e347b7810/examples/machine-code/multiword[1mWorking in $(HOLDIR)/examples/machine-code/multiword[0m
]0;Holmake: ..]0;Holmake: ~/regression/cakeml-689/basis/pure]0;Holmake: ~/regression/HOL-ce7414f3a9b67a55c010a5194ca0029e347b7810/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-ce7414f3a9b67a55c010a5194ca0029e347b7810/examples/balanced_bst]0;Holmake: ~/regression/HOL-ce7414f3a9b67a55c010a5194ca0029e347b7810/examples/balanced_bst[1mWorking in $(HOLDIR)/examples/balanced_bst[0m
]0;Holmake: ~/regression/HOL-ce7414f3a9b67a55c010a5194ca0029e347b7810/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-ce7414f3a9b67a55c010a5194ca0029e347b7810/examples/formal-languages]0;Holmake: ~/regression/HOL-ce7414f3a9b67a55c010a5194ca0029e347b7810/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-ce7414f3a9b67a55c010a5194ca0029e347b7810/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-ce7414f3a9b67a55c010a5194ca0029e347b7810/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-ce7414f3a9b67a55c010a5194ca0029e347b7810/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/HOL-ce7414f3a9b67a55c010a5194ca0029e347b7810/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-ce7414f3a9b67a55c010a5194ca0029e347b7810/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ~/regression/cakeml-689/basis/pure]0;Holmake: ~/regression/cakeml-689/misc]0;Holmake: ~/regression/HOL-ce7414f3a9b67a55c010a5194ca0029e347b7810/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-ce7414f3a9b67a55c010a5194ca0029e347b7810/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/regression/cakeml-689/misc]0;Holmake: ~/regression/cakeml-689/developers]0;Holmake: ~/regression/cakeml-689/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-689/misc]0;Holmake: ~/regression/cakeml-689/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-689/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-689/misc]0;Holmake: ~/regression/cakeml-689/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ~/regression/cakeml-689/basis/pure]0;Holmake: ~/regression/cakeml-689/basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ..]0;Holmake: ../reg_alloc]0;Holmake: ~/regression/cakeml-689/translator/monadic/monad_base]0;Holmake: ~/regression/cakeml-689/semantics]0;Holmake: ~/regression/cakeml-689/semantics/ffi]0;Holmake: ~/regression/cakeml-689/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression/cakeml-689/semantics]0;Holmake: ~/regression/cakeml-689/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ~/regression/cakeml-689/translator/monadic/monad_base]0;Holmake: ~/regression/cakeml-689/translator/monadic/monad_base[1mWorking in $(CAKEMLDIR)/translator/monadic/monad_base[0m
]0;Holmake: ../reg_alloc]0;Holmake: ~/regression/cakeml-689/unverified/reg_alloc]0;Holmake: ~/regression/cakeml-689/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-ce7414f3a9b67a55c010a5194ca0029e347b7810/examples/l3-machine-code/common]0;Holmake: ~/regression/HOL-ce7414f3a9b67a55c010a5194ca0029e347b7810/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-689/semantics/proofs]0;Holmake: ~/regression/cakeml-689/semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ..]0;Holmake: ..[1mWorking in $(CAKEMLDIR)/compiler/backend[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/compiler/backend/semantics[0m
Starting work on backendPropsTheory
Starting work on closSemTheory
Starting work on flatSemTheory
Starting work on wordSemTheory
backendPropsTheory                                                                                         OK
Starting work on patSemTheory
flatSemTheory                                                                                              OK
Starting work on flatPropsTheory
closSemTheory                                                                                              OK
Starting work on bvlSemTheory
patSemTheory                                                                                               OK
Starting work on closPropsTheory
bvlSemTheory                                                                                               OK
Starting work on bviSemTheory
wordSemTheory                                                                                              OK
Starting work on dataSemTheory
bviSemTheory                                                                                               OK
Starting work on targetSemTheory
dataSemTheory                                                                                              OK
Starting work on dataPropsTheory
flatPropsTheory                                                                                            OK
Starting work on patPropsTheory
targetSemTheory                                                                                            OK
Starting work on labSemTheory
labSemTheory                                                                                               OK
Starting work on labPropsTheory
patPropsTheory                                                                                             OK
Starting work on stackSemTheory
stackSemTheory                                                                                             OK
Starting work on stackPropsTheory
labPropsTheory                                                                                             OK
Starting work on targetPropsTheory
targetPropsTheory                                                                                          OK
Starting work on wordPropsTheory
stackPropsTheory                                                                                           OK
Starting work on README.md
README.md                                                                                                  OK
dataPropsTheory                                                                                            OK
closPropsTheory                                                                                            OK
Starting work on bvlPropsTheory
wordPropsTheory                                                                                   FAILED! <1>
     locals_rel temp s t  EVERY (x. x < temp) ls 
     locals_rel temp (alist_insert ls vs s) (alist_insert ls vs t)
 
 failed.
 First unsolved sub-goal is
 
 lookup x (alist_insert [] vs s) = lookup x (alist_insert [] vs t)
 
 Failed to prove theorem locals_rel_alist_insert.
 Uncaught exception: HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
bvlPropsTheory                                                                                       M-KILLED