Overview

Job 11

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

 Claimed job
 Starting semantics/ffi
 Finished semantics/ffi                                            9s   0kB
 Starting semantics
 Finished semantics                                             1m09s   0kB
 Starting semantics/proofs
 Finished semantics/proofs                                      1m47s   0kB
 Starting basis/pure
 Finished basis/pure                                              34s   0kB
 Starting translator
 Finished translator                                            3m41s   0kB
 Starting compiler/parsing
 Finished compiler/parsing                                      1m25s   0kB
 Starting characteristic
 Finished characteristic                                        2m11s   0kB
 Starting basis
 Finished basis                                                15m03s   0kB
 Starting translator/monadic
 Finished translator/monadic                                    1m44s   0kB
 Starting compiler/inference
 Finished compiler/inference                                    1m13s   0kB
 Starting compiler/backend/reg_alloc
 Finished compiler/backend/reg_alloc                              24s   0kB
 Starting compiler/backend/gc
 Finished compiler/backend/gc                                   7m10s   0kB
 Starting compiler/backend
 Finished compiler/backend                                         3s   0kB
 Starting compiler/encoders/asm
 Finished compiler/encoders/asm                                    0s   0kB
 Starting compiler/encoders/x64
 Finished compiler/encoders/x64                                   13s   0kB
 Starting compiler/encoders/arm6
 Finished compiler/encoders/arm6                                  46s   0kB
 Starting compiler/encoders/arm8
 Finished compiler/encoders/arm8                                   7s   0kB
 Starting compiler/encoders/mips
 Finished compiler/encoders/mips                                   9s   0kB
 Starting compiler/encoders/riscv
 Finished compiler/encoders/riscv                                  8s   0kB
 Starting compiler/backend/x64
 Finished compiler/backend/x64                                    24s   0kB
 Starting compiler/backend/arm6
 Finished compiler/backend/arm6                                   24s   0kB
 Starting compiler/backend/arm8
 Finished compiler/backend/arm8                                   24s   0kB
 Starting compiler/backend/mips
 Finished compiler/backend/mips                                   23s   0kB
 Starting compiler/backend/riscv
 Finished compiler/backend/riscv                                  25s   0kB
 Starting compiler/parsing/proofs
 Finished compiler/parsing/proofs                               5m57s   0kB
 Starting compiler/inference/proofs
 Finished compiler/inference/proofs                             2m14s   0kB
 Starting compiler/backend/semantics
 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