Job 686

CakeML:4c7bf47ab5ec3da9da1e0f994b560d0342f6e9e1
  Merge pull request #604 from Gaj7/master [Jan 16 14:54:23]
HOL:769d390effb6bfbcea7b18f4ebb2aef98afa3645
  Merge pull request #641 from immler/develop [Jan 16 06:03:18]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Jan 17 01:09:08 Claimed job
Jan 17 01:09:33 Building HOL
Jan 17 01:18:52 Starting developers
Jan 17 01:18:55 Finished developers                                               2s  20MB
Jan 17 01:18:55 Starting developers/bin
Jan 17 01:20:07 Finished developers/bin                                        1m11s 916MB
Jan 17 01:20:08 Starting semantics/ffi
Jan 17 01:20:46 Finished semantics/ffi                                           37s 320MB
Jan 17 01:20:46 Starting semantics
Jan 17 01:22:25 Finished semantics                                             1m37s 933MB
Jan 17 01:22:25 Starting semantics/proofs
Jan 17 01:25:45 Finished semantics/proofs                                      3m19s   1GB
Jan 17 01:25:46 Starting basis/pure
Jan 17 01:29:24 Finished basis/pure                                            3m37s 672MB
Jan 17 01:29:24 Starting translator
Jan 17 01:31:07 Finished translator                                            1m41s   1GB
Jan 17 01:31:07 Starting compiler/parsing
Jan 17 01:32:11 Finished compiler/parsing                                      1m03s   1GB
Jan 17 01:32:12 Starting characteristic
Jan 17 01:35:33 Finished characteristic                                        3m20s   1GB
Jan 17 01:35:34 Starting translator/monadic
Jan 17 01:37:02 Finished translator/monadic                                    1m27s   1GB
Jan 17 01:37:03 Starting basis
Jan 17 01:53:06 Finished basis                                                16m02s   2GB
Jan 17 01:53:07 Starting compiler/inference
Jan 17 01:55:04 Finished compiler/inference                                    1m56s   1GB
Jan 17 01:55:05 Starting compiler/backend/reg_alloc
Jan 17 01:55:58 Finished compiler/backend/reg_alloc                              52s   1GB
Jan 17 01:55:58 Starting compiler/backend/gc
Jan 17 02:05:00 Finished compiler/backend/gc                                   9m01s   2GB
Jan 17 02:05:01 Starting compiler/backend
Jan 17 02:05:04 Finished compiler/backend                                         2s  15MB
Jan 17 02:05:05 Starting compiler/encoders/asm
Jan 17 02:05:07 Finished compiler/encoders/asm                                    1s  17MB
Jan 17 02:05:08 Starting compiler/encoders/x64
Jan 17 02:06:10 Finished compiler/encoders/x64                                 1m01s 892MB
Jan 17 02:06:11 Starting compiler/encoders/arm6
Jan 17 02:08:03 Finished compiler/encoders/arm6                                1m51s   1GB
Jan 17 02:08:03 Starting compiler/encoders/arm8
Jan 17 02:08:35 Finished compiler/encoders/arm8                                  31s 513MB
Jan 17 02:08:36 Starting compiler/encoders/mips
Jan 17 02:09:43 Finished compiler/encoders/mips                                1m05s 788MB
Jan 17 02:09:43 Starting compiler/encoders/riscv
Jan 17 02:10:51 Finished compiler/encoders/riscv                               1m06s 838MB
Jan 17 02:10:51 Starting compiler/encoders/ag32
Jan 17 02:11:09 Finished compiler/encoders/ag32                                  17s 831MB
Jan 17 02:11:10 Starting compiler/backend/x64
Jan 17 02:11:28 Finished compiler/backend/x64                                    17s 834MB
Jan 17 02:11:29 Starting compiler/backend/arm6
Jan 17 02:11:50 Finished compiler/backend/arm6                                   20s   1GB
Jan 17 02:11:50 Starting compiler/backend/arm8
Jan 17 02:12:08 Finished compiler/backend/arm8                                   17s 861MB
Jan 17 02:12:09 Starting compiler/backend/mips
Jan 17 02:12:29 Finished compiler/backend/mips                                   19s   1GB
Jan 17 02:12:29 Starting compiler/backend/riscv
Jan 17 02:12:48 Finished compiler/backend/riscv                                  17s 969MB
Jan 17 02:12:49 Starting compiler/backend/ag32
Jan 17 02:14:02 Finished compiler/backend/ag32                                 1m12s   1GB
Jan 17 02:14:02 Starting compiler/parsing/proofs
Jan 17 02:20:01 Finished compiler/parsing/proofs                               5m57s 816MB
Jan 17 02:20:01 Starting compiler/inference/proofs
Jan 17 02:22:56 Finished compiler/inference/proofs                             2m54s   1GB
Jan 17 02:22:57 Starting compiler/backend/semantics
Jan 17 02:28:17 FAILED: compiler/backend/semantics
]0;Holmake: ~/oven/regression/HOL-769d390effb6bfbcea7b18f4ebb2aef98afa3645/examples/machine-code/multiword]0;Holmake: ~/oven/regression/HOL-769d390effb6bfbcea7b18f4ebb2aef98afa3645/examples/machine-code/multiwordWorking in $(HOLDIR)/examples/machine-code/multiword
]0;Holmake: ..]0;Holmake: ~/oven/regression/cakeml-686/basis/pure]0;Holmake: ~/oven/regression/HOL-769d390effb6bfbcea7b18f4ebb2aef98afa3645/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-769d390effb6bfbcea7b18f4ebb2aef98afa3645/examples/balanced_bst]0;Holmake: ~/oven/regression/HOL-769d390effb6bfbcea7b18f4ebb2aef98afa3645/examples/balanced_bstWorking in $(HOLDIR)/examples/balanced_bst
]0;Holmake: ~/oven/regression/HOL-769d390effb6bfbcea7b18f4ebb2aef98afa3645/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-769d390effb6bfbcea7b18f4ebb2aef98afa3645/examples/formal-languages]0;Holmake: ~/oven/regression/HOL-769d390effb6bfbcea7b18f4ebb2aef98afa3645/examples/formal-languagesWorking in $(HOLDIR)/examples/formal-languages
]0;Holmake: ~/oven/regression/HOL-769d390effb6bfbcea7b18f4ebb2aef98afa3645/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-769d390effb6bfbcea7b18f4ebb2aef98afa3645/examples/formal-languages/context-free]0;Holmake: ~/oven/regression/HOL-769d390effb6bfbcea7b18f4ebb2aef98afa3645/examples/formal-languages/context-freeWorking in $(HOLDIR)/examples/formal-languages/context-free
]0;Holmake: ~/oven/regression/HOL-769d390effb6bfbcea7b18f4ebb2aef98afa3645/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-769d390effb6bfbcea7b18f4ebb2aef98afa3645/examples/formal-languages/regularWorking in $(HOLDIR)/examples/formal-languages/regular
]0;Holmake: ~/oven/regression/cakeml-686/basis/pure]0;Holmake: ~/oven/regression/cakeml-686/misc]0;Holmake: ~/oven/regression/HOL-769d390effb6bfbcea7b18f4ebb2aef98afa3645/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/oven/regression/HOL-769d390effb6bfbcea7b18f4ebb2aef98afa3645/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: ~/oven/regression/cakeml-686/misc]0;Holmake: ~/oven/regression/cakeml-686/developers]0;Holmake: ~/oven/regression/cakeml-686/developersWorking in $(CAKEMLDIR)/developers
]0;Holmake: ~/oven/regression/cakeml-686/misc]0;Holmake: ~/oven/regression/cakeml-686/misc/lem_lib_stub]0;Holmake: ~/oven/regression/cakeml-686/misc/lem_lib_stubWorking in $(CAKEMLDIR)/misc/lem_lib_stub
]0;Holmake: ~/oven/regression/cakeml-686/misc]0;Holmake: ~/oven/regression/cakeml-686/miscWorking in $(CAKEMLDIR)/misc
]0;Holmake: ~/oven/regression/cakeml-686/basis/pure]0;Holmake: ~/oven/regression/cakeml-686/basis/pureWorking in $(CAKEMLDIR)/basis/pure
]0;Holmake: ..]0;Holmake: ../reg_alloc]0;Holmake: ~/oven/regression/cakeml-686/translator/monadic/monad_base]0;Holmake: ~/oven/regression/cakeml-686/semantics]0;Holmake: ~/oven/regression/cakeml-686/semantics/ffi]0;Holmake: ~/oven/regression/cakeml-686/semantics/ffiWorking in $(CAKEMLDIR)/semantics/ffi
]0;Holmake: ~/oven/regression/cakeml-686/semantics]0;Holmake: ~/oven/regression/cakeml-686/semanticsWorking in $(CAKEMLDIR)/semantics
]0;Holmake: ~/oven/regression/cakeml-686/translator/monadic/monad_base]0;Holmake: ~/oven/regression/cakeml-686/translator/monadic/monad_baseWorking in $(CAKEMLDIR)/translator/monadic/monad_base
]0;Holmake: ../reg_alloc]0;Holmake: ~/oven/regression/cakeml-686/unverified/reg_alloc]0;Holmake: ~/oven/regression/cakeml-686/unverified/reg_allocWorking in $(CAKEMLDIR)/unverified/reg_alloc
]0;Holmake: ../reg_alloc]0;Holmake: ../reg_allocWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc
]0;Holmake: ..]0;Holmake: ../../encoders/asm]0;Holmake: ~/oven/regression/HOL-769d390effb6bfbcea7b18f4ebb2aef98afa3645/examples/l3-machine-code/common]0;Holmake: ~/oven/regression/HOL-769d390effb6bfbcea7b18f4ebb2aef98afa3645/examples/l3-machine-code/commonWorking in $(HOLDIR)/examples/l3-machine-code/common
]0;Holmake: ../../encoders/asm]0;Holmake: ../../encoders/asmWorking in $(CAKEMLDIR)/compiler/encoders/asm
]0;Holmake: ..]0;Holmake: ~/oven/regression/cakeml-686/semantics/proofs]0;Holmake: ~/oven/regression/cakeml-686/semantics/proofsWorking in $(CAKEMLDIR)/semantics/proofs
]0;Holmake: ..]0;Holmake: ..Working in $(CAKEMLDIR)/compiler/backend
]0;Holmake: .]0;Holmake: .Working in $(CAKEMLDIR)/compiler/backend/semantics
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
wordSemTheory                                                                OK
Starting work on dataSemTheory
bvlSemTheory                                                                 OK
Starting work on bviSemTheory
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