Job 11

CakeML:7f9f024bedaa89b1dd3bd371cf03ced2ab8310c1
  Adjust data_to_word to fit syntactic criteria [Nov 10 00:00:00]
#366 (i2w_w2i_32bit)
Merging into:c382040c6f947d8309996fbbb2d23912b8a00cf4
  Fix riscv to_dataBootstrap - main prog renamed [Nov 10 00:00:00]
HOL:adf95fed567e76641363a906871d9110e3d12f71
  Useful functions for dealing with terms up-to aconv [Nov 08 00:00:00]
Machine:cse-gmeza 4.13.10-200.fc26.x86_64 x86_64 GNU/Linux

Nov 10 15:01:02 Claimed job
Nov 10 15:01:08 Starting semantics/ffi
Nov 10 15:01:18 Finished semantics/ffi                                            9s   0kB
Nov 10 15:01:18 Starting semantics
Nov 10 15:02:47 Finished semantics                                             1m09s   0kB
Nov 10 15:02:47 Starting semantics/proofs
Nov 10 15:04:36 Finished semantics/proofs                                      1m47s   0kB
Nov 10 15:04:36 Starting basis/pure
Nov 10 15:05:11 Finished basis/pure                                              34s   0kB
Nov 10 15:05:11 Starting translator
Nov 10 15:09:13 Finished translator                                            3m41s   0kB
Nov 10 15:09:13 Starting compiler/parsing
Nov 10 15:10:39 Finished compiler/parsing                                      1m25s   0kB
Nov 10 15:10:39 Starting characteristic
Nov 10 15:12:51 Finished characteristic                                        2m11s   0kB
Nov 10 15:12:52 Starting basis
Nov 10 15:27:56 Finished basis                                                15m03s   0kB
Nov 10 15:27:56 Starting translator/monadic
Nov 10 15:29:40 Finished translator/monadic                                    1m44s   0kB
Nov 10 15:29:41 Starting compiler/inference
Nov 10 15:30:54 Finished compiler/inference                                    1m13s   0kB
Nov 10 15:30:55 Starting compiler/backend/reg_alloc
Nov 10 15:31:19 Finished compiler/backend/reg_alloc                              24s   0kB
Nov 10 15:31:20 Starting compiler/backend/gc
Nov 10 15:38:50 Finished compiler/backend/gc                                   7m10s   0kB
Nov 10 15:38:51 Starting compiler/backend
Nov 10 15:38:55 Finished compiler/backend                                         3s   0kB
Nov 10 15:38:55 Starting compiler/encoders/asm
Nov 10 15:38:55 Finished compiler/encoders/asm                                    0s   0kB
Nov 10 15:38:56 Starting compiler/encoders/x64
Nov 10 15:39:29 Finished compiler/encoders/x64                                   13s   0kB
Nov 10 15:39:30 Starting compiler/encoders/arm6
Nov 10 15:40:16 Finished compiler/encoders/arm6                                  46s   0kB
Nov 10 15:40:17 Starting compiler/encoders/arm8
Nov 10 15:40:24 Finished compiler/encoders/arm8                                   7s   0kB
Nov 10 15:40:25 Starting compiler/encoders/mips
Nov 10 15:40:34 Finished compiler/encoders/mips                                   9s   0kB
Nov 10 15:40:34 Starting compiler/encoders/riscv
Nov 10 15:40:43 Finished compiler/encoders/riscv                                  8s   0kB
Nov 10 15:40:43 Starting compiler/backend/x64
Nov 10 15:41:07 Finished compiler/backend/x64                                    24s   0kB
Nov 10 15:41:08 Starting compiler/backend/arm6
Nov 10 15:41:33 Finished compiler/backend/arm6                                   24s   0kB
Nov 10 15:41:33 Starting compiler/backend/arm8
Nov 10 15:41:57 Finished compiler/backend/arm8                                   24s   0kB
Nov 10 15:42:17 Starting compiler/backend/mips
Nov 10 15:42:41 Finished compiler/backend/mips                                   23s   0kB
Nov 10 15:42:41 Starting compiler/backend/riscv
Nov 10 15:43:06 Finished compiler/backend/riscv                                  25s   0kB
Nov 10 15:43:27 Starting compiler/parsing/proofs
Nov 10 15:49:25 Finished compiler/parsing/proofs                               5m57s   0kB
Nov 10 15:49:25 Starting compiler/inference/proofs
Nov 10 15:51:40 Finished compiler/inference/proofs                             2m14s   0kB
Nov 10 15:51:40 Starting compiler/backend/semantics
Nov 10 15:52:30 FAILED: compiler/backend/semantics
]0;Holmake: ..Recursively calling Holmake in /home/agomezl/PhD/cake/regression/HOL/examples/machine-code/multiword
]0;Holmake: ~/PhD/cake/regression/HOL/examples/machine-code/multiwordRecursively calling Holmake in /home/agomezl/PhD/cake/regression/HOL/examples/machine-code/hoare-triple
]0;Holmake: ~/PhD/cake/regression/HOL/examples/machine-code/hoare-triple]0;Holmake: ~/PhD/cake/regression/HOL/examples/machine-code/hoare-tripleFinished recursive invocation in /home/agomezl/PhD/cake/regression/HOL/examples/machine-code/hoare-triple
]0;Holmake: ~/PhD/cake/regression/HOL/examples/machine-code/multiword]0;Holmake: ~/PhD/cake/regression/HOL/examples/machine-code/multiwordFinished recursive invocation in /home/agomezl/PhD/cake/regression/HOL/examples/machine-code/multiword
]0;Holmake: ..Recursively calling Holmake in ../../../basis/pure
]0;Holmake: ../../../basis/pureRecursively calling Holmake in /home/agomezl/PhD/cake/regression/HOL/examples/formal-languages/regular
]0;Holmake: ~/PhD/cake/regression/HOL/examples/formal-languages/regularRecursively calling Holmake in /home/agomezl/PhD/cake/regression/HOL/examples/balanced_bst
]0;Holmake: ~/PhD/cake/regression/HOL/examples/balanced_bst]0;Holmake: ~/PhD/cake/regression/HOL/examples/balanced_bstFinished recursive invocation in /home/agomezl/PhD/cake/regression/HOL/examples/balanced_bst
]0;Holmake: ~/PhD/cake/regression/HOL/examples/formal-languages/regularRecursively calling Holmake in /home/agomezl/PhD/cake/regression/HOL/examples/formal-languages
]0;Holmake: ~/PhD/cake/regression/HOL/examples/formal-languages]0;Holmake: ~/PhD/cake/regression/HOL/examples/formal-languagesFinished recursive invocation in /home/agomezl/PhD/cake/regression/HOL/examples/formal-languages
]0;Holmake: ~/PhD/cake/regression/HOL/examples/formal-languages/regularRecursively calling Holmake in /home/agomezl/PhD/cake/regression/HOL/examples/formal-languages/context-free
]0;Holmake: ~/PhD/cake/regression/HOL/examples/formal-languages/context-free]0;Holmake: ~/PhD/cake/regression/HOL/examples/formal-languages/context-freeFinished recursive invocation in /home/agomezl/PhD/cake/regression/HOL/examples/formal-languages/context-free
]0;Holmake: ~/PhD/cake/regression/HOL/examples/formal-languages/regular]0;Holmake: ~/PhD/cake/regression/HOL/examples/formal-languages/regularStarting work on regexp2dfa
regexp2dfa                                                                   OK
Finished recursive invocation in /home/agomezl/PhD/cake/regression/HOL/examples/formal-languages/regular
]0;Holmake: ../../../basis/pureRecursively calling Holmake in ../../../misc
]0;Holmake: ../../../miscRecursively calling Holmake in /home/agomezl/PhD/cake/regression/HOL/examples/fun-op-sem/lprefix_lub
]0;Holmake: ~/PhD/cake/regression/HOL/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/PhD/cake/regression/HOL/examples/fun-op-sem/lprefix_lubFinished recursive invocation in /home/agomezl/PhD/cake/regression/HOL/examples/fun-op-sem/lprefix_lub
]0;Holmake: ../../../miscRecursively calling Holmake in ../../../developers
]0;Holmake: ../../../developers]0;Holmake: ../../../developersFinished recursive invocation in ../../../developers
]0;Holmake: ../../../miscRecursively calling Holmake in ../../../misc/lem_lib_stub
]0;Holmake: ../../../misc/lem_lib_stub]0;Holmake: ../../../misc/lem_lib_stubFinished recursive invocation in ../../../misc/lem_lib_stub
]0;Holmake: ../../../misc]0;Holmake: ../../../miscFinished recursive invocation in ../../../misc
]0;Holmake: ../../../basis/pure]0;Holmake: ../../../basis/pureFinished recursive invocation in ../../../basis/pure
]0;Holmake: ..Recursively calling Holmake in ../reg_alloc
]0;Holmake: ../reg_allocRecursively calling Holmake in ../../../unverified/reg_alloc
]0;Holmake: ../../../unverified/reg_alloc]0;Holmake: ../../../unverified/reg_allocFinished recursive invocation in ../../../unverified/reg_alloc
]0;Holmake: ../reg_alloc]0;Holmake: ../reg_allocFinished recursive invocation in ../reg_alloc
]0;Holmake: ..Recursively calling Holmake in ../../encoders
]0;Holmake: ../../encoders]0;Holmake: ../../encodersFinished recursive invocation in ../../encoders
]0;Holmake: ..Recursively calling Holmake in ../../encoders/asm
]0;Holmake: ../../encoders/asmRecursively calling Holmake in /home/agomezl/PhD/cake/regression/HOL/examples/l3-machine-code/common
]0;Holmake: ~/PhD/cake/regression/HOL/examples/l3-machine-code/common]0;Holmake: ~/PhD/cake/regression/HOL/examples/l3-machine-code/commonFinished recursive invocation in /home/agomezl/PhD/cake/regression/HOL/examples/l3-machine-code/common
]0;Holmake: ../../encoders/asmRecursively calling Holmake in ../../../semantics
]0;Holmake: ../../../semanticsRecursively calling Holmake in ../../../semantics/ffi
]0;Holmake: ../../../semantics/ffi]0;Holmake: ../../../semantics/ffiFinished recursive invocation in ../../../semantics/ffi
]0;Holmake: ../../../semantics]0;Holmake: ../../../semanticsFinished recursive invocation in ../../../semantics
]0;Holmake: ../../encoders/asm]0;Holmake: ../../encoders/asmFinished recursive invocation in ../../encoders/asm
]0;Holmake: ..]0;Holmake: ..Finished recursive invocation in ..
]0;Holmake: .Recursively calling Holmake in ../../../semantics/proofs
]0;Holmake: ../../../semantics/proofs]0;Holmake: ../../../semantics/proofsFinished recursive invocation in ../../../semantics/proofs
]0;Holmake: .]0;Holmake: .Starting work on closSemTheory
Starting work on conSemTheory
Starting work on exhSemTheory
Starting work on targetSemTheory
targetSemTheory                                                              OK
Starting work on wordSemTheory
conSemTheory                                                                 OK
Starting work on conPropsTheory
exhSemTheory                                                                 OK
Starting work on decSemTheory
closSemTheory                                                                OK
Starting work on bvlSemTheory
decSemTheory                                                                 OK
Starting work on closPropsTheory
wordSemTheory                                                                OK
Starting work on labSemTheory
bvlSemTheory                                                                 OK
Starting work on bviSemTheory
labSemTheory                                                        FAILED! <1>
   pattern completion has added 2 clauses to the original specification.>>
 <<HOL message: mk_functional:
   pattern completion has added 4 clauses to the original specification.>>
 <<HOL message: mk_functional:
   pattern completion has added 3 clauses to the original specification.>>
 Saved definition __ "evaluate_def"
 Saved induction ___ "evaluate_ind"
 Saved definition __ "semantics_def"
 Exporting theory "labSem" ... done.
 Theory "labSem" took 9.4s to build
conPropsTheory                                                         M-KILLED
closPropsTheory                                                        M-KILLED
bviSemTheory                                                           M-KILLED