CakeML:dbe52948f62b25903830503113aa22020be2c8a0
Port the tutorial exercise generator to CakeML
#459 (issue380)
Merging into:d10e991231ff3b75fb86fc7051192c92751501ae
Make process term mlstring instead of string
HOL:60830f02ff6b86e0fd69ce6679614d497089b2eb
Merge branch 'master' of https://github.com/HOL-Theorem-Prover/HOL
Machine:cakeml1796 4.4.0-22-generic x86_64 GNU/Linux
Claimed job
Building HOL
Starting semantics/ffi
Finished semantics/ffi 1m05s 498MB
Starting semantics
FAILED: semantics
]0;Holmake: /scratch/cakeml/regression/HOL-60830f02ff6b86e0fd69ce6679614d497089b2eb/examples/formal-languages/context-free]0;Holmake: /scratch/cakeml/regression/HOL-60830f02ff6b86e0fd69ce6679614d497089b2eb/examples/formal-languages/context-freeFinished recursive invocation in /scratch/cakeml/regression/HOL-60830f02ff6b86e0fd69ce6679614d497089b2eb/examples/formal-languages/context-free
]0;Holmake: .Recursively calling Holmake in /scratch/cakeml/regression/HOL-60830f02ff6b86e0fd69ce6679614d497089b2eb/examples/fun-op-sem/lprefix_lub
]0;Holmake: /scratch/cakeml/regression/HOL-60830f02ff6b86e0fd69ce6679614d497089b2eb/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL-60830f02ff6b86e0fd69ce6679614d497089b2eb/examples/fun-op-sem/lprefix_lubStarting work on lprefix_lubTheory
lprefix_lubTheory OK
Finished recursive invocation in /scratch/cakeml/regression/HOL-60830f02ff6b86e0fd69ce6679614d497089b2eb/examples/fun-op-sem/lprefix_lub
]0;Holmake: .Recursively calling Holmake in ../misc
]0;Holmake: ../miscRecursively calling Holmake in /scratch/cakeml/regression/HOL-60830f02ff6b86e0fd69ce6679614d497089b2eb/examples/machine-code/hoare-triple
]0;Holmake: /scratch/cakeml/regression/HOL-60830f02ff6b86e0fd69ce6679614d497089b2eb/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/HOL-60830f02ff6b86e0fd69ce6679614d497089b2eb/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 /scratch/cakeml/regression/HOL-60830f02ff6b86e0fd69ce6679614d497089b2eb/examples/machine-code/hoare-triple
]0;Holmake: ../miscRecursively calling Holmake in ../developers
]0;Holmake: ../developersRecursively calling Holmake in ../compiler/bootstrap/compilation/x64/64
]0;Holmake: ../compiler/bootstrap/compilation/x64/64Recursively calling Holmake in ../basis
]0;Holmake: ../basisRecursively calling Holmake in ../basis/pure
]0;Holmake: ../basis/pureRecursively calling Holmake in /scratch/cakeml/regression/HOL-60830f02ff6b86e0fd69ce6679614d497089b2eb/examples/formal-languages/regular
]0;Holmake: /scratch/cakeml/regression/HOL-60830f02ff6b86e0fd69ce6679614d497089b2eb/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-60830f02ff6b86e0fd69ce6679614d497089b2eb/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/HOL-60830f02ff6b86e0fd69ce6679614d497089b2eb/examples/balanced_bst]0;Holmake: /scratch/cakeml/regression/HOL-60830f02ff6b86e0fd69ce6679614d497089b2eb/examples/balanced_bstStarting work on balanced_mapTheory
balanced_mapTheory OK
Starting work on osetTheory
osetTheory OK
Finished recursive invocation in /scratch/cakeml/regression/HOL-60830f02ff6b86e0fd69ce6679614d497089b2eb/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/HOL-60830f02ff6b86e0fd69ce6679614d497089b2eb/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-60830f02ff6b86e0fd69ce6679614d497089b2eb/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-60830f02ff6b86e0fd69ce6679614d497089b2eb/examples/formal-languages]0;Holmake: /scratch/cakeml/regression/HOL-60830f02ff6b86e0fd69ce6679614d497089b2eb/examples/formal-languagesStarting work on FormalLangTheory
FormalLangTheory OK
Finished recursive invocation in /scratch/cakeml/regression/HOL-60830f02ff6b86e0fd69ce6679614d497089b2eb/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-60830f02ff6b86e0fd69ce6679614d497089b2eb/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-60830f02ff6b86e0fd69ce6679614d497089b2eb/examples/formal-languages/regularStarting work on charsetTheory
Starting work on eq_cmp_bmapTheory
Starting work on vec_mapTheory
vec_mapTheory OK
eq_cmp_bmapTheory OK
charsetTheory OK
Starting work on regexpTheory
regexpTheory OK
Starting work on regexp_compilerTheory
Starting work on regexp_parserTheory
regexp_parserTheory OK
regexp_compilerTheory OK
Starting work on regexp2dfa
regexp2dfa OK
Finished recursive invocation in /scratch/cakeml/regression/HOL-60830f02ff6b86e0fd69ce6679614d497089b2eb/examples/formal-languages/regular
]0;Holmake: ../basis/pure]0;Holmake: ../basis/pureDon't know how to build necessary target(s): /scratch/cakeml/regression/cakeml-224/misc/preamble.uo, /scratch/cakeml/regression/cakeml-224/misc/miscTheory.uo, /scratch/cakeml/regression/cakeml-224/misc/miscTheory.ui
Finished recursive invocation in ../basis/pure
]0;Holmake: ../basisFinished recursive invocation in ../basis
]0;Holmake: ../compiler/bootstrap/compilation/x64/64Finished recursive invocation in ../compiler/bootstrap/compilation/x64/64
]0;Holmake: ../developersFinished recursive invocation in ../developers
]0;Holmake: ../miscFinished recursive invocation in ../misc
]0;Holmake: .