CakeML:dddc90697053484d9719b005cc06edb0624ea1ff Precompute charset_sing for grepHOL:ca8e9a987cc46d3eb40c776d94464e4a5939b2e5 Fix Unicode in previous commit; add RATN & RATD constants to rat thyMachine:cakeml1796 4.4.0-22-generic x86_64 GNU/Linux Claimed job Building HOL Starting semantics/ffi Finished semantics/ffi 1m13s 314MB Starting semantics Finished semantics 2m56s 1GB Starting semantics/proofs Finished semantics/proofs 3m50s 1GB Starting basis/pure Finished basis/pure 6m38s 663MB Starting translator FAILED: translator ]0;Holmake: ../basis/pureRecursively calling Holmake in /scratch/cakeml/regression/HOL/examples/formal-languages/regular ]0;Holmake: /scratch/cakeml/regression/HOL/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL/examples/balanced_bst ]0;Holmake: /scratch/cakeml/regression/HOL/examples/balanced_bst]0;Holmake: /scratch/cakeml/regression/HOL/examples/balanced_bstFinished recursive invocation in /scratch/cakeml/regression/HOL/examples/balanced_bst ]0;Holmake: /scratch/cakeml/regression/HOL/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL/examples/formal-languages ]0;Holmake: /scratch/cakeml/regression/HOL/examples/formal-languages]0;Holmake: /scratch/cakeml/regression/HOL/examples/formal-languagesFinished recursive invocation in /scratch/cakeml/regression/HOL/examples/formal-languages ]0;Holmake: /scratch/cakeml/regression/HOL/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL/examples/formal-languages/context-free ]0;Holmake: /scratch/cakeml/regression/HOL/examples/formal-languages/context-free]0;Holmake: /scratch/cakeml/regression/HOL/examples/formal-languages/context-freeFinished recursive invocation in /scratch/cakeml/regression/HOL/examples/formal-languages/context-free ]0;Holmake: /scratch/cakeml/regression/HOL/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL/examples/formal-languages/regularFinished recursive invocation in /scratch/cakeml/regression/HOL/examples/formal-languages/regular ]0;Holmake: ../basis/pureRecursively calling Holmake in ../misc ]0;Holmake: ../miscRecursively calling Holmake in /scratch/cakeml/regression/HOL/examples/fun-op-sem/lprefix_lub ]0;Holmake: /scratch/cakeml/regression/HOL/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL/examples/fun-op-sem/lprefix_lubFinished recursive invocation in /scratch/cakeml/regression/HOL/examples/fun-op-sem/lprefix_lub ]0;Holmake: ../miscRecursively calling Holmake in /scratch/cakeml/regression/HOL/examples/machine-code/hoare-triple ]0;Holmake: /scratch/cakeml/regression/HOL/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/HOL/examples/machine-code/hoare-tripleFinished recursive invocation in /scratch/cakeml/regression/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: ../basis/pure]0;Holmake: ../basis/pureFinished recursive invocation in ../basis/pure ]0;Holmake: .Recursively 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: .Recursively calling Holmake in ../semantics/alt_semantics ]0;Holmake: ../semantics/alt_semantics]0;Holmake: ../semantics/alt_semanticsStarting work on heap heap OK Starting work on smallStepTheory smallStepTheory OK Starting work on bigStepTheory bigStepTheory OK Finished recursive invocation in ../semantics/alt_semantics ]0;Holmake: .Recursively calling Holmake in ../semantics/alt_semantics/proofs ]0;Holmake: ../semantics/alt_semantics/proofsRecursively calling Holmake in ../semantics/proofs ]0;Holmake: ../semantics/proofs]0;Holmake: ../semantics/proofsFinished recursive invocation in ../semantics/proofs ]0;Holmake: ../semantics/alt_semantics/proofs]0;Holmake: ../semantics/alt_semantics/proofsStarting work on heap heap OK Starting work on determTheory Starting work on bigSmallInvariantsTheory Starting work on bigStepPropsTheory bigSmallInvariantsTheory OK determTheory OK Starting work on bigClockTheory bigStepPropsTheory OK bigClockTheory OK Starting work on bigSmallEquivTheory Starting work on interpTheory interpTheory OK Starting work on funBigStepEquivTheory funBigStepEquivTheory OK bigSmallEquivTheory OK Starting work on untypedSafetyTheory untypedSafetyTheory OK Finished recursive invocation in ../semantics/alt_semantics/proofs ]0;Holmake: .]0;Holmake: .Starting work on heap heap OK Starting work on ml_progTheory ml_progTheory OK Starting work on ml_translatorTheory ml_translatorTheory FAILED! <1> Proof of env x1 x2 a n v. Eval env x1 (VECTOR_TYPE a v) Eval env x2 (NUM n) n < length v Eval env (App Vsub [x1; x2]) (a (sub v n)) failed. Failed to prove theorem Eval_sub.