Overview

Job 8

CakeML:772ea4647099cbae61aea97eda95190d61facb9a
  Bootstrap (x64) eval files for riscv
#352 (arm6_export)
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
 FAILED: semantics
]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: .Recursively 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: .Recursively calling Holmake in ../misc
]0;Holmake: ../miscRecursively 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: ../miscRecursively calling Holmake in ../developers
]0;Holmake: ../developers]0;Holmake: ../developersStarting work on readme_gen
readme_gen                                                                   OK
Starting work on README.md
README.md                                                                    OK
Finished 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: ../miscStarting work on README.md
Starting work on miscTheory
README.md                                                                    OK
miscTheory                                                                   OK
Finished recursive invocation in ../misc
]0;Holmake: .Recursively calling Holmake in ffi
]0;Holmake: ffi]0;Holmake: ffiFinished recursive invocation in ffi
]0;Holmake: .]0;Holmake: .Starting work on addancs
Starting work on heap
addancs                                                                      OK
Starting work on astScript
Starting work on namespaceScript
Starting work on tokensScript
namespaceScript                                                              OK
astScript                                                                    OK
tokensScript                                                                 OK
heap                                                                         OK
Starting work on fpSemTheory
Starting work on namespaceTheory
Starting work on tokensTheory
fpSemTheory                                                                  OK
tokensTheory                                                                 OK
Starting work on gramTheory
Starting work on tokenUtilsTheory
Starting work on lexer_funTheory
namespaceTheory                                                              OK
Starting work on astTheory
astTheory                                                                    OK
Starting work on semanticPrimitivesTheory
gramTheory                                                                   OK
tokenUtilsTheory                                                             OK
Starting work on cmlPtreeConversionTheory
semanticPrimitivesTheory                                                     OK
Starting work on evaluateTheory
Starting work on typeSystemTheory
evaluateTheory                                                      FAILED! <1>
 Saved definition __ "envLift_def"
 <<HOL warning: GrammarDeltas.revise_data:
   Grammar-deltas:
     overload_on("evaluate_tops_tupled")
   invalidated by DelConstant(evaluate$evaluate_tops_tupled)>>
 Saved definition __ "evaluate_tops_def"
 Saved induction ___ "evaluate_tops_ind"
 Saved definition __ "evaluate_prog_def"
 Exporting theory "evaluate" ... done.
 Theory "evaluate" took 2.1s to build
lexer_funTheory                                                        M-KILLED
cmlPtreeConversionTheory                                               M-KILLED
typeSystemTheory                                                       M-KILLED