Job 685

CakeML:4c7bf47ab5ec3da9da1e0f994b560d0342f6e9e1
  Merge pull request #604 from Gaj7/master [Jan 16 14:54:23]
HOL:1ffe69b178c3c393e0f5453ac2f1ca3fbc7c7b42
  Add selftest for sorting_compset [Jan 15 02:02:25]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Jan 16 16:06:46 Claimed job
Jan 16 16:06:50 Reusing HOL
Jan 16 16:07:44 Starting developers
Jan 16 16:07:47 Finished developers                                               2s  19MB
Jan 16 16:07:48 Starting developers/bin
Jan 16 16:09:00 Finished developers/bin                                        1m11s 916MB
Jan 16 16:09:01 Starting semantics/ffi
Jan 16 16:09:11 Finished semantics/ffi                                           10s 216MB
Jan 16 16:09:12 Starting semantics
Jan 16 16:10:36 Finished semantics                                             1m23s   1GB
Jan 16 16:10:37 Starting semantics/proofs
Jan 16 16:13:54 Finished semantics/proofs                                      3m16s   1GB
Jan 16 16:13:54 Starting basis/pure
Jan 16 16:14:48 Finished basis/pure                                              52s 673MB
Jan 16 16:14:49 Starting translator
Jan 16 16:16:32 Finished translator                                            1m41s   1GB
Jan 16 16:16:32 Starting compiler/parsing
Jan 16 16:17:37 Finished compiler/parsing                                      1m03s   1GB
Jan 16 16:17:37 Starting characteristic
Jan 16 16:20:58 Finished characteristic                                        3m19s   1GB
Jan 16 16:20:58 Starting translator/monadic
Jan 16 16:22:26 Finished translator/monadic                                    1m27s   1GB
Jan 16 16:22:27 Starting basis
Jan 16 16:38:30 Finished basis                                                16m02s   2GB
Jan 16 16:38:31 Starting compiler/inference
Jan 16 16:40:11 Finished compiler/inference                                    1m39s   1GB
Jan 16 16:40:11 Starting compiler/backend/reg_alloc
Jan 16 16:41:05 Finished compiler/backend/reg_alloc                              53s   1GB
Jan 16 16:41:06 Starting compiler/backend/gc
Jan 16 16:49:04 Finished compiler/backend/gc                                   7m57s   1GB
Jan 16 16:49:05 Starting compiler/backend
Jan 16 16:49:08 Finished compiler/backend                                         2s  23MB
Jan 16 16:49:09 Starting compiler/encoders/asm
Jan 16 16:49:11 Finished compiler/encoders/asm                                    1s  20MB
Jan 16 16:49:11 Starting compiler/encoders/x64
Jan 16 16:49:37 Finished compiler/encoders/x64                                   25s 644MB
Jan 16 16:49:38 Starting compiler/encoders/arm6
Jan 16 16:50:33 Finished compiler/encoders/arm6                                  55s   1GB
Jan 16 16:50:34 Starting compiler/encoders/arm8
Jan 16 16:50:48 Finished compiler/encoders/arm8                                  13s 550MB
Jan 16 16:50:48 Starting compiler/encoders/mips
Jan 16 16:51:06 Finished compiler/encoders/mips                                  17s 881MB
Jan 16 16:51:07 Starting compiler/encoders/riscv
Jan 16 16:51:22 Finished compiler/encoders/riscv                                 14s 708MB
Jan 16 16:51:22 Starting compiler/encoders/ag32
Jan 16 16:51:40 Finished compiler/encoders/ag32                                  17s 814MB
Jan 16 16:51:41 Starting compiler/backend/x64
Jan 16 16:51:59 Finished compiler/backend/x64                                    18s   1GB
Jan 16 16:52:00 Starting compiler/backend/arm6
Jan 16 16:52:20 Finished compiler/backend/arm6                                   19s   1GB
Jan 16 16:52:20 Starting compiler/backend/arm8
Jan 16 16:52:39 Finished compiler/backend/arm8                                   17s 849MB
Jan 16 16:52:39 Starting compiler/backend/mips
Jan 16 16:52:59 Finished compiler/backend/mips                                   19s   1GB
Jan 16 16:53:00 Starting compiler/backend/riscv
Jan 16 16:53:20 Finished compiler/backend/riscv                                  18s   1GB
Jan 16 16:53:20 Starting compiler/backend/ag32
Jan 16 16:54:33 Finished compiler/backend/ag32                                 1m11s   1GB
Jan 16 16:54:34 Starting compiler/parsing/proofs
Jan 16 17:00:34 Finished compiler/parsing/proofs                               5m59s 946MB
Jan 16 17:00:34 Starting compiler/inference/proofs
Jan 16 17:03:29 Finished compiler/inference/proofs                             2m53s   1GB
Jan 16 17:03:29 Starting compiler/backend/semantics
Jan 16 17:08:48 FAILED: compiler/backend/semantics
]0;Holmake: ~/oven/regression/HOL-1ffe69b178c3c393e0f5453ac2f1ca3fbc7c7b42/examples/machine-code/multiword]0;Holmake: ~/oven/regression/HOL-1ffe69b178c3c393e0f5453ac2f1ca3fbc7c7b42/examples/machine-code/multiwordWorking in $(HOLDIR)/examples/machine-code/multiword
]0;Holmake: ..]0;Holmake: ~/oven/regression/cakeml-685/basis/pure]0;Holmake: ~/oven/regression/HOL-1ffe69b178c3c393e0f5453ac2f1ca3fbc7c7b42/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-1ffe69b178c3c393e0f5453ac2f1ca3fbc7c7b42/examples/balanced_bst]0;Holmake: ~/oven/regression/HOL-1ffe69b178c3c393e0f5453ac2f1ca3fbc7c7b42/examples/balanced_bstWorking in $(HOLDIR)/examples/balanced_bst
]0;Holmake: ~/oven/regression/HOL-1ffe69b178c3c393e0f5453ac2f1ca3fbc7c7b42/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-1ffe69b178c3c393e0f5453ac2f1ca3fbc7c7b42/examples/formal-languages]0;Holmake: ~/oven/regression/HOL-1ffe69b178c3c393e0f5453ac2f1ca3fbc7c7b42/examples/formal-languagesWorking in $(HOLDIR)/examples/formal-languages
]0;Holmake: ~/oven/regression/HOL-1ffe69b178c3c393e0f5453ac2f1ca3fbc7c7b42/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-1ffe69b178c3c393e0f5453ac2f1ca3fbc7c7b42/examples/formal-languages/context-free]0;Holmake: ~/oven/regression/HOL-1ffe69b178c3c393e0f5453ac2f1ca3fbc7c7b42/examples/formal-languages/context-freeWorking in $(HOLDIR)/examples/formal-languages/context-free
]0;Holmake: ~/oven/regression/HOL-1ffe69b178c3c393e0f5453ac2f1ca3fbc7c7b42/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-1ffe69b178c3c393e0f5453ac2f1ca3fbc7c7b42/examples/formal-languages/regularWorking in $(HOLDIR)/examples/formal-languages/regular
]0;Holmake: ~/oven/regression/cakeml-685/basis/pure]0;Holmake: ~/oven/regression/cakeml-685/misc]0;Holmake: ~/oven/regression/HOL-1ffe69b178c3c393e0f5453ac2f1ca3fbc7c7b42/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/oven/regression/HOL-1ffe69b178c3c393e0f5453ac2f1ca3fbc7c7b42/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: ~/oven/regression/cakeml-685/misc]0;Holmake: ~/oven/regression/cakeml-685/developers]0;Holmake: ~/oven/regression/cakeml-685/developersWorking in $(CAKEMLDIR)/developers
]0;Holmake: ~/oven/regression/cakeml-685/misc]0;Holmake: ~/oven/regression/cakeml-685/misc/lem_lib_stub]0;Holmake: ~/oven/regression/cakeml-685/misc/lem_lib_stubWorking in $(CAKEMLDIR)/misc/lem_lib_stub
]0;Holmake: ~/oven/regression/cakeml-685/misc]0;Holmake: ~/oven/regression/cakeml-685/miscWorking in $(CAKEMLDIR)/misc
]0;Holmake: ~/oven/regression/cakeml-685/basis/pure]0;Holmake: ~/oven/regression/cakeml-685/basis/pureWorking in $(CAKEMLDIR)/basis/pure
]0;Holmake: ..]0;Holmake: ../reg_alloc]0;Holmake: ~/oven/regression/cakeml-685/translator/monadic/monad_base]0;Holmake: ~/oven/regression/cakeml-685/semantics]0;Holmake: ~/oven/regression/cakeml-685/semantics/ffi]0;Holmake: ~/oven/regression/cakeml-685/semantics/ffiWorking in $(CAKEMLDIR)/semantics/ffi
]0;Holmake: ~/oven/regression/cakeml-685/semantics]0;Holmake: ~/oven/regression/cakeml-685/semanticsWorking in $(CAKEMLDIR)/semantics
]0;Holmake: ~/oven/regression/cakeml-685/translator/monadic/monad_base]0;Holmake: ~/oven/regression/cakeml-685/translator/monadic/monad_baseWorking in $(CAKEMLDIR)/translator/monadic/monad_base
]0;Holmake: ../reg_alloc]0;Holmake: ~/oven/regression/cakeml-685/unverified/reg_alloc]0;Holmake: ~/oven/regression/cakeml-685/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-1ffe69b178c3c393e0f5453ac2f1ca3fbc7c7b42/examples/l3-machine-code/common]0;Holmake: ~/oven/regression/HOL-1ffe69b178c3c393e0f5453ac2f1ca3fbc7c7b42/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-685/semantics/proofs]0;Holmake: ~/oven/regression/cakeml-685/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
closSemTheory                                                                OK
Starting work on bvlSemTheory
flatSemTheory                                                                OK
Starting work on closPropsTheory
patSemTheory                                                                 OK
Starting work on dataSemTheory
bvlSemTheory                                                                 OK
Starting work on bviSemTheory
wordSemTheory                                                                OK
Starting work on flatPropsTheory
dataSemTheory                                                                OK
Starting work on dataPropsTheory
bviSemTheory                                                                 OK
Starting work on targetSemTheory
targetSemTheory                                                              OK
Starting work on labSemTheory
flatPropsTheory                                                              OK
Starting work on patPropsTheory
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
dataPropsTheory                                                              OK
Starting work on README.md
README.md                                                                    OK
stackPropsTheory                                                             OK
closPropsTheory                                                              OK
Starting work on bvlPropsTheory
wordPropsTheory                                                     FAILED! <1>
 Exception raised at Tactical.TAC_PROOF:
 unsolved goals
 error in quse /home/cake/oven/regression/cakeml-685/compiler/backend/semantics/wordPropsScript.sml : HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
 error in load wordPropsScript : HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
 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