CakeML:c382040c6f947d8309996fbbb2d23912b8a00cf4
Fix riscv to_dataBootstrap - main prog renamed
HOL:adf95fed567e76641363a906871d9110e3d12f71
Useful functions for dealing with terms up-to aconv
Machine:gemma 4.13.11-gnu-1 x86_64 GNU/Linux
Claimed job
Starting semantics/ffi
Finished semantics/ffi 44s 420MB
Starting semantics
FAILED: semantics
]0;Holmake: ~/cakeml-worker/HOL/examples/formal-languages/context-free]0;Holmake: ~/cakeml-worker/HOL/examples/formal-languages/context-freeFinished recursive invocation in /home/ramana/cakeml-worker/HOL/examples/formal-languages/context-free
]0;Holmake: .Recursively calling Holmake in /home/ramana/cakeml-worker/HOL/examples/fun-op-sem/lprefix_lub
]0;Holmake: ~/cakeml-worker/HOL/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/cakeml-worker/HOL/examples/fun-op-sem/lprefix_lubStarting work on lprefix_lubTheory
lprefix_lubTheory OK
Finished recursive invocation in /home/ramana/cakeml-worker/HOL/examples/fun-op-sem/lprefix_lub
]0;Holmake: .Recursively calling Holmake in ../misc
]0;Holmake: ../miscRecursively calling Holmake in /home/ramana/cakeml-worker/HOL/examples/machine-code/hoare-triple
]0;Holmake: ~/cakeml-worker/HOL/examples/machine-code/hoare-triple]0;Holmake: ~/cakeml-worker/HOL/examples/machine-code/hoare-tripleStarting work on set_sepTheory
Starting work on tailrecTheory
tailrecTheory OK
set_sepTheory OK
Starting work on progTheory
progTheory OK
Starting work on addressTheory
Starting work on temporalTheory
temporalTheory OK
addressTheory OK
Finished recursive invocation in /home/ramana/cakeml-worker/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
astScript OK
namespaceScript 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 FAILED! <1>
Saved theorem _____ "MMLnonT_induction"
<<HOL message: Defined type: "MMLnonT">>
Saved definition __ "cmlG_def"
Saved theorem _____ "nt_distinct_ths"
Saved definition __ "Ndl_def"
Saved definition __ "Lfl_def"
runtime: 9.6s, gctime: 1.4s, systime: 0.31655s.
valid_ptree: OK
Exporting theory "gram" ... done.
Theory "gram" took 11.2s to build
tokenUtilsTheory M-KILLED
lexer_funTheory M-KILLED
semanticPrimitivesTheory M-KILLED
Machine: gemma 4.13.11-gnu-1 x86_64 GNU/Linux
2017-11-11T07:47:14Z Claimed job
2017-11-11T07:47:19Z Building HOL
2017-11-11T07:47:27Z Starting semantics/ffi
2017-11-11T07:47:40Z Finished semantics/ffi 11.55 299288
2017-11-11T07:47:41Z Starting semantics
2017-11-11T07:49:12Z Finished semantics 89.72 1113580
2017-11-11T07:49:13Z Starting semantics/proofs
2017-11-11T07:49:41Z FAILED: semantics/proofs
Recursively calling Holmake in /home/ramana/cakeml-worker/HOL/examples/formal-languages/context-free
]0;Holmake: ~/cakeml-worker/HOL/examples/formal-languages/context-free]0;Holmake: ~/cakeml-worker/HOL/examples/formal-languages/context-freeFinished recursive invocation in /home/ramana/cakeml-worker/HOL/examples/formal-languages/context-free
]0;Holmake: .Recursively calling Holmake in ../../misc
]0;Holmake: ../../miscRecursively calling Holmake in /home/ramana/cakeml-worker/HOL/examples/fun-op-sem/lprefix_lub
]0;Holmake: ~/cakeml-worker/HOL/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/cakeml-worker/HOL/examples/fun-op-sem/lprefix_lubFinished recursive invocation in /home/ramana/cakeml-worker/HOL/examples/fun-op-sem/lprefix_lub
]0;Holmake: ../../miscRecursively calling Holmake in /home/ramana/cakeml-worker/HOL/examples/machine-code/hoare-triple
]0;Holmake: ~/cakeml-worker/HOL/examples/machine-code/hoare-triple]0;Holmake: ~/cakeml-worker/HOL/examples/machine-code/hoare-tripleFinished recursive invocation in /home/ramana/cakeml-worker/HOL/examples/machine-code/hoare-triple
]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: .Recursively calling Holmake in ..
]0;Holmake: ..Recursively calling Holmake in ../ffi
]0;Holmake: ../ffi]0;Holmake: ../ffiFinished recursive invocation in ../ffi
]0;Holmake: ..]0;Holmake: ..Finished recursive invocation in ..
]0;Holmake: .]0;Holmake: .Starting work on heap
heap OK
Starting work on astPropsTheory
Starting work on gramPropsTheory
Starting work on semanticPrimitivesPropsTheory
Starting work on typeSoundInvariantsTheory
typeSoundInvariantsTheory OK
astPropsTheory FAILED! <1>
<<HOL message: Created theory "astProps">>
Exporting theory "astProps" ... done.
Theory "astProps" took 0.00098s to build
gramPropsTheory M-KILLED
semanticPrimitivesPropsTheory M-KILLED
Machine: gemma 4.13.11-gnu-1 x86_64 GNU/Linux
2017-11-11T10:58:21Z Claimed job
2017-11-11T10:58:26Z Building HOL
2017-11-11T11:02:15Z FAILED: building HOL