CakeML:d10e991231ff3b75fb86fc7051192c92751501ae
Make process term mlstring instead of string
HOL:60830f02ff6b86e0fd69ce6679614d497089b2eb
Merge branch 'master' of https://github.com/HOL-Theorem-Prover/HOL
Machine:cakeml1794 4.4.0-98-generic x86_64 GNU/Linux
Claimed job
Building HOL
Starting semantics/ffi
Finished semantics/ffi 1m07s 499MB
Starting semantics
Finished semantics 2m34s 1GB
Starting semantics/proofs
Finished semantics/proofs 3m30s 1GB
Starting basis/pure
Finished basis/pure 6m14s 649MB
Starting translator
FAILED: translator
]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_bstFinished 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-languagesFinished recursive invocation in /scratch/cakeml/regression/HOL-60830f02ff6b86e0fd69ce6679614d497089b2eb/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-60830f02ff6b86e0fd69ce6679614d497089b2eb/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-60830f02ff6b86e0fd69ce6679614d497089b2eb/examples/formal-languages/context-free
]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: /scratch/cakeml/regression/HOL-60830f02ff6b86e0fd69ce6679614d497089b2eb/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-60830f02ff6b86e0fd69ce6679614d497089b2eb/examples/formal-languages/regularFinished recursive invocation in /scratch/cakeml/regression/HOL-60830f02ff6b86e0fd69ce6679614d497089b2eb/examples/formal-languages/regular
]0;Holmake: ../basis/pureRecursively calling Holmake in ../misc
]0;Holmake: ../miscRecursively 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_lubFinished recursive invocation in /scratch/cakeml/regression/HOL-60830f02ff6b86e0fd69ce6679614d497089b2eb/examples/fun-op-sem/lprefix_lub
]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-tripleFinished recursive invocation in /scratch/cakeml/regression/HOL-60830f02ff6b86e0fd69ce6679614d497089b2eb/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 bigStepScript
Starting work on heap
bigStepScript OK
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
Starting work on bigSmallInvariantsScript
bigSmallInvariantsScript OK
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>
error in load ml_translatorScript : HOL_ERR {message = " (THEN1 on line 112)", origin_function = "DISCH_THEN", origin_structure = "Thm_cont"}
Uncaught exception: HOL_ERR {message = " (THEN1 on line 112)", origin_function = "DISCH_THEN", origin_structure = "Thm_cont"}
Proof of
evaluate F env (empty_state with refs := s.refs) exp
(empty_state with refs := s.refs refs',Rval x)
evaluate F env s exp (s with refs := s.refs refs',Rval x)
failed.
Failed to prove theorem evaluate_empty_state_IMP.