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