Job 230

CakeML:0b7197a3eeeccad25727f909bf9a1db4d704e902
  Isabelle adaptation without 'undefined' [Feb 06 09:30:08]
#453 (larsrh-3)
Merging into:37a8fbbfaf51a828ac12526de8b07e7c12292231
  Merge pull request #462 from ncough/basis_fix [Feb 22 07:04:02]
HOL:8630df6da54f64f8b648bd9bc047ff0928b0e72c
  tactictoe: minor fix [Feb 22 18:24:10]
Machine:cakeml1794 4.4.0-98-generic x86_64 GNU/Linux

Feb 23 00:12:14 Claimed job
Feb 23 00:12:23 Building HOL
Feb 23 00:24:50 Starting semantics/ffi
Feb 23 00:26:00 Finished semantics/ffi                                         1m07s 408MB
Feb 23 00:26:01 Starting semantics
Feb 23 00:28:41 Finished semantics                                             2m37s   1GB
Feb 23 00:28:43 Starting semantics/proofs
Feb 23 00:32:15 Finished semantics/proofs                                      3m29s 960MB
Feb 23 00:32:17 Starting basis/pure
Feb 23 00:38:33 Finished basis/pure                                            6m13s 607MB
Feb 23 00:38:35 Starting translator
Feb 23 00:43:27 FAILED: translator
]0;Holmake: ../basis/pureRecursively calling Holmake in /scratch/cakeml/regression/HOL-8630df6da54f64f8b648bd9bc047ff0928b0e72c/examples/formal-languages/regular
]0;Holmake: /scratch/cakeml/regression/HOL-8630df6da54f64f8b648bd9bc047ff0928b0e72c/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-8630df6da54f64f8b648bd9bc047ff0928b0e72c/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/HOL-8630df6da54f64f8b648bd9bc047ff0928b0e72c/examples/balanced_bst]0;Holmake: /scratch/cakeml/regression/HOL-8630df6da54f64f8b648bd9bc047ff0928b0e72c/examples/balanced_bstFinished recursive invocation in /scratch/cakeml/regression/HOL-8630df6da54f64f8b648bd9bc047ff0928b0e72c/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/HOL-8630df6da54f64f8b648bd9bc047ff0928b0e72c/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-8630df6da54f64f8b648bd9bc047ff0928b0e72c/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-8630df6da54f64f8b648bd9bc047ff0928b0e72c/examples/formal-languages]0;Holmake: /scratch/cakeml/regression/HOL-8630df6da54f64f8b648bd9bc047ff0928b0e72c/examples/formal-languagesFinished recursive invocation in /scratch/cakeml/regression/HOL-8630df6da54f64f8b648bd9bc047ff0928b0e72c/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-8630df6da54f64f8b648bd9bc047ff0928b0e72c/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-8630df6da54f64f8b648bd9bc047ff0928b0e72c/examples/formal-languages/context-free
]0;Holmake: /scratch/cakeml/regression/HOL-8630df6da54f64f8b648bd9bc047ff0928b0e72c/examples/formal-languages/context-free]0;Holmake: /scratch/cakeml/regression/HOL-8630df6da54f64f8b648bd9bc047ff0928b0e72c/examples/formal-languages/context-freeFinished recursive invocation in /scratch/cakeml/regression/HOL-8630df6da54f64f8b648bd9bc047ff0928b0e72c/examples/formal-languages/context-free
]0;Holmake: /scratch/cakeml/regression/HOL-8630df6da54f64f8b648bd9bc047ff0928b0e72c/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-8630df6da54f64f8b648bd9bc047ff0928b0e72c/examples/formal-languages/regularFinished recursive invocation in /scratch/cakeml/regression/HOL-8630df6da54f64f8b648bd9bc047ff0928b0e72c/examples/formal-languages/regular
]0;Holmake: ../basis/pureRecursively calling Holmake in ../misc
]0;Holmake: ../miscRecursively calling Holmake in /scratch/cakeml/regression/HOL-8630df6da54f64f8b648bd9bc047ff0928b0e72c/examples/fun-op-sem/lprefix_lub
]0;Holmake: /scratch/cakeml/regression/HOL-8630df6da54f64f8b648bd9bc047ff0928b0e72c/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL-8630df6da54f64f8b648bd9bc047ff0928b0e72c/examples/fun-op-sem/lprefix_lubFinished recursive invocation in /scratch/cakeml/regression/HOL-8630df6da54f64f8b648bd9bc047ff0928b0e72c/examples/fun-op-sem/lprefix_lub
]0;Holmake: ../miscRecursively calling Holmake in /scratch/cakeml/regression/HOL-8630df6da54f64f8b648bd9bc047ff0928b0e72c/examples/machine-code/hoare-triple
]0;Holmake: /scratch/cakeml/regression/HOL-8630df6da54f64f8b648bd9bc047ff0928b0e72c/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/HOL-8630df6da54f64f8b648bd9bc047ff0928b0e72c/examples/machine-code/hoare-tripleFinished recursive invocation in /scratch/cakeml/regression/HOL-8630df6da54f64f8b648bd9bc047ff0928b0e72c/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.